1  /-
  2  Copyright (c) 2019 Johan Commelin. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Johan Commelin, Kenny Lau
  5  -/
  6  
  7  import data.finsupp order.complete_lattice algebra.ordered_group data.mv_polynomial
src         └──────────┘ └────────────────────┘ └───────────────────┘ └────────────────┘
  8  import algebra.order_functions
src         └─────────────────────┘
  9  import ring_theory.ideal_operations
src         └──────────────────────────┘
 10  
 11  /-!
 12  # Formal power series
 13  
 14  This file defines (multivariate) formal power series
 15  and develops the basic properties of these objects.
 16  
 17  A formal power series is to a polynomial like an infinite sum is to a finite sum.
 18  
 19  We provide the natural inclusion from polynomials to formal power series.
 20  
 21  ## Generalities
 22  
 23  The file starts with setting up the (semi)ring structure on multivariate power series.
 24  
 25  `trunc n φ` truncates a formal power series to the polynomial
 26  that has the same coefficients as φ, for all m ≤ n, and 0 otherwise.
 27  
 28  If the constant coefficient of a formal power series is invertible,
 29  then this formal power series is invertible.
 30  
 31  Formal power series over a local ring form a local ring.
 32  
 33  ## Formal power series in one variable
 34  
 35  We prove that if the ring of coefficients is an integral domain,
 36  then formal power series in one variable form an integral domain.
 37  
 38  The `order` of a formal power series `φ` is the multiplicity of the variable `X` in `φ`.
 39  
 40  If the coefficients form an integral domain, then `order` is a valuation
 41  (`order_mul`, `order_add_ge`).
 42  
 43  ## Implementation notes
 44  
 45  In this file we define multivariate formal power series with
 46  variables indexed by `σ` and coefficients in `α` as
 47  mv_power_series σ α := (σ →₀ ℕ) → α.
 48  Unfortunately there is not yet enough API to show that they are the completion
 49  of the ring of multivariate polynomials. However, we provide most of the infrastructure
 50  that is needed to do this. Once I-adic completion (topological or algebraic) is available
 51  it should not be hard to fill in the details.
 52  
 53  Formal power series in one variable are defined as
 54  power_series α := mv_power_series unit α.
 55  
 56  This allows us to port a lot of proofs and properties
 57  from the multivariate case to the single variable case.
 58  However, it means that formal power series are indexed by (unit →₀ ℕ),
 59  which is of course canonically isomorphic to ℕ.
 60  We then build some glue to treat formal power series as if they are indexed by ℕ.
 61  Occasionally this leads to proofs that are uglier than expected.
 62  
 63  -/
 64  
 65  noncomputable theory
 66  open_locale classical
 67  
 68  /-- Multivariate formal power series, where `σ` is the index set of the variables
 69  and `α` is the coefficient ring.-/
 70  def mv_power_series (σ : Type*) (α : Type*) := (σ →₀ ℕ) → α
id                                                    └┘     
src                                                    └┘ 
typ                                                   └┘     
doc                                                    └┘
 71  
 72  namespace mv_power_series
 73  open finsupp
 74  variables {σ : Type*} {α : Type*}
 75  
 76  instance [inhabited α]       : inhabited       (mv_power_series σ α) := ⟨λ _, default _⟩
id             └───────┘           └───────┘        └─────────────┘            └─────┘
src            └───────┘            └───────┘        └─────────────┘               └─────┘
typ            └───────┘           └───────┘        └─────────────┘            └─────┘
doc                                                  └─────────────┘
 77  instance [has_zero α]        : has_zero        (mv_power_series σ α) := pi.has_zero
id             └──────┘            └──────┘         └─────────────┘       └─────────┘
src            └──────┘             └──────┘         └─────────────┘         └─────────┘
typ            └──────┘            └──────┘         └─────────────┘       └─────────┘
doc                                                  └─────────────┘
 78  instance [add_monoid α]      : add_monoid      (mv_power_series σ α) := pi.add_monoid
id             └────────┘          └────────┘       └─────────────┘       └───────────┘
src            └────────┘           └────────┘       └─────────────┘         └───────────┘
typ            └────────┘          └────────┘       └─────────────┘       └───────────┘
doc                                                  └─────────────┘
 79  instance [add_group α]       : add_group       (mv_power_series σ α) := pi.add_group
id             └───────┘           └───────┘        └─────────────┘       └──────────┘
src            └───────┘            └───────┘        └─────────────┘         └──────────┘
typ            └───────┘           └───────┘        └─────────────┘       └──────────┘
doc                                                  └─────────────┘
 80  instance [add_comm_monoid α] : add_comm_monoid (mv_power_series σ α) := pi.add_comm_monoid
id             └─────────────┘     └─────────────┘  └─────────────┘       └────────────────┘
src            └─────────────┘      └─────────────┘  └─────────────┘         └────────────────┘
typ            └─────────────┘     └─────────────┘  └─────────────┘       └────────────────┘
doc                                                  └─────────────┘
 81  instance [add_comm_group α]  : add_comm_group  (mv_power_series σ α) := pi.add_comm_group
id             └────────────┘      └────────────┘   └─────────────┘       └───────────────┘
src            └────────────┘       └────────────┘   └─────────────┘         └───────────────┘
typ            └────────────┘      └────────────┘   └─────────────┘       └───────────────┘
doc                                                  └─────────────┘
 82  
 83  section add_monoid
 84  variables [add_monoid α]
id              └────────┘
src             └────────┘
typ             └────────┘
 85  
 86  variables (α)
 87  
 88  /-- The `n`th monomial with coefficient `a` as multivariate formal power series.-/
 89  def monomial (n : σ →₀ ℕ) : α →+ mv_power_series σ α :=
id                      └┘      └┘ └─────────────┘  
src                      └┘       └┘ └─────────────┘
typ                     └┘      └┘ └─────────────┘  
doc                      └┘        └┘ └─────────────┘
 90  { to_fun := λ a m, if m = n then a else 0,
id                               
src                          
typ                              
 91    map_zero' := funext $ λ m, by { split_ifs; refl },
id                  └────┘     
src                 └────┘             └───────┘  └───┘
typ                 └────┘            └───────┘  └───┘
doc                                    └───────┘  └───┘
txt                                    └───────┘  └───┘
par                                    └───────┘  └───┘
pid                                                   
st                                  └─────────────────┘└┘
 92    map_add' := λ a b, funext $ λ m,
id                      └────┘     
src                       └────┘
typ                     └────┘     
 93      show (if m = n then a + b else 0) = (if m = n then a else 0) + (if m = n then b else 0),
id                                                                      
src                                                                      
typ                                                                     
 94      from if h : m = n then by simp only [if_pos h] else by simp only [if_neg h, add_zero] }
id            └┘                           └────┘                      └────┘   └──────┘
src           └┘                  └─────────┘└────┘ └┘        └─────────┘└────┘ └┘└──────┘└┘
typ           └┘                └─────────┘└────┘└┘        └─────────┘└────┘└┘└──────┘└┘
doc                                └─────────┘       └┘        └─────────┘       └┘        └┘
txt                                └─────────┘       └┘        └─────────┘       └┘        └┘
par                                └─────────┘       └┘        └─────────┘       └┘        └┘
pid                                    └──┘└┘                   └──┘└┘       └┘        
st                                └────────────────────┘       └──────────────────────────────┘
 95  
 96  /-- The `n`th coefficient of a multivariate formal power series.-/
 97  def coeff (n : σ →₀ ℕ) : (mv_power_series σ α) →+ α :=
id                   └┘      └─────────────┘    └┘ 
src                   └┘      └─────────────┘      └┘
typ                  └┘      └─────────────┘    └┘ 
doc                   └┘       └─────────────┘      └┘
 98  { to_fun := λ φ, φ n,
id                    
typ                   
 99    map_zero' := rfl,
id                  └─┘
src                 └─┘
typ                 └─┘
100    map_add' := λ _ _, rfl }
id                      └─┘
src                       └─┘
typ                     └─┘
101  
102  variables {α}
103  
104  /-- Two multivariate formal power series are equal if all their coefficients are equal.-/
105  @[ext] lemma ext {φ ψ} (h : ∀ (n : σ →₀ ℕ), coeff α n φ = coeff α n ψ) :
id                                       └┘    └───┘     └───┘   
src                                       └┘    └───┘        └───┘
typ                                      └┘    └───┘     └───┘   
doc    └─┘                                └┘     └───┘         └───┘
106    φ = ψ :=
id       
src      
typ      
107  funext h
id   └────┘ 
src  └────┘
typ  └────┘ 
108  
109  /-- Two multivariate formal power series are equal
110   if and only if all their coefficients are equal.-/
111  lemma ext_iff {φ ψ : mv_power_series σ α} :
id                        └─────────────┘  
src                       └─────────────┘
typ                       └─────────────┘  
doc                       └─────────────┘
112    φ = ψ ↔ (∀ (n : σ →₀ ℕ), coeff α n φ = coeff α n ψ) :=
id                  └┘    └───┘     └───┘   
src                    └┘    └───┘        └───┘
typ                 └┘    └───┘     └───┘   
doc                      └┘     └───┘         └───┘
113  ⟨λ h n, congr_arg (coeff α n) h, ext⟩
id         └───────┘  └───┘      └─┘
src          └───────┘  └───┘         └─┘
typ        └───────┘  └───┘      └─┘
doc                     └───┘         └─┘
114  
115  lemma coeff_monomial (m n : σ →₀ ℕ) (a : α) :
id                                └┘        
src                                └┘ 
typ                               └┘        
doc                                └┘
116    coeff α m (monomial α n a) = if m = n then a else 0 := rfl
id     └───┘    └──────┘                            └─┘
src    └───┘      └──────┘                                  └─┘
typ    └───┘    └──────┘                            └─┘
doc    └───┘      └──────┘
117  
118  @[simp] lemma coeff_monomial' (n : σ →₀ ℕ) (a : α) :
id                                       └┘        
src                                       └┘ 
typ                                      └┘        
doc    └──┘                               └┘
119    coeff α n (monomial α n a) = a := if_pos rfl
id     └───┘    └──────┘          └────┘ └─┘
src    └───┘      └──────┘              └────┘ └─┘
typ    └───┘    └──────┘          └────┘ └─┘
doc    └───┘      └──────┘
120  
121  @[simp] lemma coeff_comp_monomial (n : σ →₀ ℕ) :
id                                           └┘ 
src                                           └┘ 
typ                                          └┘ 
doc    └──┘                                   └┘
122    (coeff α n).comp (monomial α n) = add_monoid_hom.id α :=
id      └───┘   └──┘   └──────┘     └───────────────┘ 
src     └───┘     └──┘   └──────┘       └───────────────┘
typ     └───┘   └──┘   └──────┘     └───────────────┘ 
doc     └───┘            └──────┘
123  add_monoid_hom.ext $ coeff_monomial' n
id   └────────────────┘   └─────────────┘ 
src  └────────────────┘   └─────────────┘
typ  └────────────────┘   └─────────────┘ 
124  
125  @[simp] lemma coeff_zero (n : σ →₀ ℕ) : coeff α n (0 : mv_power_series σ α) = 0 := rfl
id                                  └┘     └───┘        └─────────────┘          └─┘
src                                  └┘     └───┘          └─────────────┘            └─┘
typ                                 └┘     └───┘        └─────────────┘          └─┘
doc    └──┘                          └┘      └───┘          └─────────────┘
126  
127  end add_monoid
128  
129  section semiring
130  variables [semiring α] (n : σ →₀ ℕ) (φ ψ : mv_power_series σ α)
id              └──────┘           └┘          └─────────────┘
src             └──────┘           └┘          └─────────────┘
typ             └──────┘           └┘          └─────────────┘
doc                                └┘           └─────────────┘
131  
132  instance : has_one (mv_power_series σ α) := ⟨monomial α (0 : σ →₀ ℕ) 1⟩
id              └─────┘  └─────────────┘        └──────┘        └┘ 
src             └─────┘  └─────────────┘          └──────┘          └┘ 
typ             └─────┘  └─────────────┘        └──────┘        └┘ 
doc                      └─────────────┘          └──────┘          └┘
133  
134  lemma coeff_one :
135    coeff α n (1 : mv_power_series σ α) = if n = 0 then 1 else 0 := rfl
id     └───┘        └─────────────┘                             └─┘
src    └───┘          └─────────────┘                                └─┘
typ    └───┘        └─────────────┘                             └─┘
doc    └───┘          └─────────────┘
136  
137  @[simp] lemma coeff_zero_one : coeff α (0 : σ →₀ ℕ) 1 = 1 :=
id                                  └───┘        └┘     
src                                 └───┘          └┘     
typ                                 └───┘        └┘     
doc    └──┘                         └───┘          └┘
138  coeff_monomial' 0 1
id   └─────────────┘
src  └─────────────┘
typ  └─────────────┘
139  
140  instance : has_mul (mv_power_series σ α) :=
id              └─────┘  └─────────────┘  
src             └─────┘  └─────────────┘
typ             └─────┘  └─────────────┘  
doc                      └─────────────┘
141  ⟨λ φ ψ n, (finsupp.antidiagonal n).support.sum (λ p, φ p.1 * ψ p.2)⟩
id           └──────────────────┘  └─────┘ └─┘            
src             └──────────────────┘   └─────┘ └─┘                 
typ          └──────────────────┘  └─────┘ └─┘            
142  
143  lemma coeff_mul : coeff α n (φ * ψ) =
id                     └───┘        
src                    └───┘            
typ                    └───┘        
doc                    └───┘
144    (finsupp.antidiagonal n).support.sum (λ p, coeff α p.1 φ * coeff α p.2 ψ) := rfl
id      └──────────────────┘  └─────┘ └─┘       └───┘      └───┘         └─┘
src     └──────────────────┘   └─────┘ └─┘        └───┘         └───┘            └─┘
typ     └──────────────────┘  └─────┘ └─┘       └───┘      └───┘         └─┘
doc                                               └───┘           └───┘
145  
146  protected lemma zero_mul : (0 : mv_power_series σ α) * φ = 0 :=
id                                   └─────────────┘      
src                                  └─────────────┘         
typ                                  └─────────────┘      
doc                                  └─────────────┘
147  ext $ λ n, by simp [coeff_mul]
id   └─┘                └───────┘
src  └─┘           └────┘└───────┘└─
typ  └─┘          └────┘└───────┘└─
doc  └─┘           └────┘         └─
txt                └────┘         └─
par                └────┘         └─
pid                             
st                └─────────────────
148  
src  
typ  
doc  
txt  
par  
pid  
st   
149  protected lemma mul_zero : φ * 0 = 0 :=
id                                  
src                                  
typ                                 
150  ext $ λ n, by simp [coeff_mul]
id   └─┘                └───────┘
src  └─┘           └────┘└───────┘└─
typ  └─┘          └────┘└───────┘└─
doc  └─┘           └────┘         └─
txt                └────┘         └─
par                └────┘         └─
pid                             
st                └─────────────────
151  
src  
typ  
doc  
txt  
par  
pid  
st   
152  protected lemma one_mul : (1 : mv_power_series σ α) * φ = φ :=
id                                  └─────────────┘       
src                                 └─────────────┘         
typ                                 └─────────────┘       
doc                                 └─────────────┘
153  ext $ λ n,
id   └─┘     
src  └─┘
typ  └─┘     
doc  └─┘
154  begin
st   └─────
155    rw [coeff_mul, finset.sum_eq_single ((0 : σ →₀ ℕ), n)];
id         └───────┘  └──────────────────┘       └┘     
src    └──┘└───────┘└┘└──────────────────┘ └──┘ └┘ └─┘ └┘
typ    └──┘└───────┘└┘└──────────────────┘ └──┘└┘ └─┘└┘
doc    └──┘         └┘                      └──┘ └┘ └─┘ └┘
txt    └──┘         └┘                      └──┘    └─┘ └┘
par    └──┘         └┘                      └──┘    └─┘ └┘
pid      └┘         └┘                      └──┘    └─┘ └┘
st   ──────────────┘└──────────────────────────────────────┘└─
156    simp [mem_antidiagonal_support, coeff_one],
id           └──────────────────────┘  └───────┘
src    └────┘└──────────────────────┘└┘└───────┘
typ    └────┘└──────────────────────┘└┘└───────┘
doc    └────┘                        └┘         
txt    └────┘                        └┘         
par    └────┘                        └┘         
pid                                └┘         
st   ───────────────────────────────────────────┘└─
157    show ∀ (i j : σ →₀ ℕ), i + j = n → (i = 0 → j ≠ n) →
id                                               
src    └───┘ └──────┘            └─┘   └┘ 
typ    └───┘ └──────┘          └─┘ └┘ 
doc    └───┘ └──────┘              └─┘    └┘ 
txt    └───┘ └──────┘              └─┘    └┘ 
par    └───┘ └──────┘              └─┘    └┘ 
pid    └───┘ └──────┘              └─┘    └┘ 
st   ───────────────────────────────────────────────────────
158      (if (i = 0) then 1 else 0) * (coeff α j) φ = 0,
id                                    └───┘     
src  ───┘      └─────────────────┘ └───┘  └┘  └┘
typ  ───┘      └─────────────────┘ └───┘ └┘ └┘
doc  ───┘      └─────────────────┘  └───┘  └┘  └┘
txt  ───┘      └─────────────────┘         └┘  └┘
par  ───┘      └─────────────────┘         └┘  └┘
pid  ───┘      └─────────────────┘         └┘  
st   ─────────────────────────────────────────────────┘└─
159    intros i j hij h,
src    └──────────────┘
typ    └──────────────┘
doc    └──────────────┘
txt    └──────────────┘
par    └──────────────┘
pid          └────────┘
st   ─────────────────┘└─
160    rw [if_neg, zero_mul],
id         └────┘  └──────┘
src    └──┘└────┘└┘└──────┘
typ    └──┘└────┘└┘└──────┘
doc    └──┘      └┘        
txt    └──┘      └┘        
par    └──┘      └┘        
pid      └┘      └┘        
st   ───────────┘└────────┘└──
161    contrapose! h,
src    └───────────┘
typ    └───────────┘
doc    └───────────┘
txt    └───────────┘
par    └───────────┘
pid              └┘
st   ──────────────┘└─
162    simpa [h] using hij,
id                    └─┘
src    └─────┘ └──────┘
typ    └─────┘└──────┘└─┘
doc    └─────┘ └──────┘
txt    └─────┘ └──────┘
par    └─────┘ └──────┘
pid          └────┘
st   ────────────────────┘└─
163  end
st   ──┘
164  
165  protected lemma mul_one : φ * 1 = φ :=
id                                  
src                                 
typ                                 
166  ext $ λ n,
id   └─┘     
src  └─┘
typ  └─┘     
doc  └─┘
167  begin
st   └─────
168    rw [coeff_mul, finset.sum_eq_single (n, (0 : σ →₀ ℕ))],
id         └───────┘  └──────────────────┘         └┘
src    └──┘└───────┘└┘└──────────────────┘ └┘ └──┘ └┘ └─┘
typ    └──┘└───────┘└┘└──────────────────┘└┘ └──┘└┘ └─┘
doc    └──┘         └┘                      └┘ └──┘ └┘ └─┘
txt    └──┘         └┘                      └┘ └──┘    └─┘
par    └──┘         └┘                      └┘ └──┘    └─┘
pid      └┘         └┘                      └┘ └──┘    └─┘
st   ──────────────┘└──────────────────────────────────────┘└──
169    rotate,
src    └────┘
typ    └────┘
doc    └────┘
txt    └────┘
par    └────┘
st   ───────┘└─
170    { rintros ⟨i, j⟩ hij h,
src      └──────────────────┘
typ      └──────────────────┘
doc      └──────────────────┘
txt      └──────────────────┘
par      └──────────────────┘
pid             └───────────┘
st   ───┘└──────────────────┘└─
171      rw [coeff_one, if_neg, mul_zero],
id           └───────┘  └────┘  └──────┘
src      └──┘└───────┘└┘└────┘└┘└──────┘
typ      └──┘└───────┘└┘└────┘└┘└──────┘
doc      └──┘         └┘      └┘        
txt      └──┘         └┘      └┘        
par      └──┘         └┘      └┘        
pid        └┘         └┘      └┘        
st   ────────────────┘└──────┘└────────┘└──
172      rw mem_antidiagonal_support at hij,
id          └──────────────────────┘
src      └─┘└──────────────────────┘└─────┘
typ      └─┘└──────────────────────┘└─────┘
doc      └─┘                        └─────┘
txt      └─┘                        └─────┘
par      └─┘                        └─────┘
pid                                └─────┘
st   ─────────────────────────────────────┘└─
173      contrapose! h,
src      └───────────┘
typ      └───────────┘
doc      └───────────┘
txt      └───────────┘
par      └───────────┘
pid                └┘
st   ────────────────┘└─
174      simpa [h] using hij },
id                      └─┘
src      └─────┘ └──────┘   
typ      └─────┘└──────┘└─┘
doc      └─────┘ └──────┘   
txt      └─────┘ └──────┘   
par      └─────┘ └──────┘   
pid            └────┘   
st   ───────────────────────┘└┘
175    all_goals { simp [mem_antidiagonal_support, coeff_one] }
id                       └──────────────────────┘  └───────┘
src    └──────────┘└────┘└──────────────────────┘└┘└───────┘└┘└┘
typ    └──────────┘└────┘└──────────────────────┘└┘└───────┘└┘└┘
doc    └──────────┘└────┘                        └┘         └┘└┘
txt    └──────────┘└────┘                        └┘         └┘└┘
par    └──────────┘└────┘                        └┘         └┘└┘
pid             └───────┘                        └┘         └─┘
st   ────────────┘└──────────────────────────────────────────┘
176  end
st   └─┘
177  
178  protected lemma mul_add (φ₁ φ₂ φ₃ : mv_power_series σ α) :
id                                       └─────────────┘  
src                                      └─────────────┘
typ                                      └─────────────┘  
doc                                      └─────────────┘
179    φ₁ * (φ₂ + φ₃) = φ₁ * φ₂ + φ₁ * φ₃ :=
id     └┘   └┘  └┘   └┘  └┘  └┘  └┘
src                             
typ    └┘   └┘  └┘   └┘  └┘  └┘  └┘
180  ext $ λ n, by simp only [coeff_mul, mul_add, finset.sum_add_distrib, add_monoid_hom.map_add]
id   └─┘                     └───────┘  └─────┘  └────────────────────┘  └────────────────────┘
src  └─┘           └─────────┘└───────┘└┘└─────┘└┘└────────────────────┘└┘└────────────────────┘└─
typ  └─┘          └─────────┘└───────┘└┘└─────┘└┘└────────────────────┘└┘└────────────────────┘└─
doc  └─┘           └─────────┘         └┘       └┘                      └┘                      └─
txt                └─────────┘         └┘       └┘                      └┘                      └─
par                └─────────┘         └┘       └┘                      └┘                      └─
pid                    └──┘└┘         └┘       └┘                      └┘                      
st                └───────────────────────────────────────────────────────────────────────────────
181  
src  
typ  
doc  
txt  
par  
pid  
st   
182  protected lemma add_mul (φ₁ φ₂ φ₃ : mv_power_series σ α) :
id                                       └─────────────┘  
src                                      └─────────────┘
typ                                      └─────────────┘  
doc                                      └─────────────┘
183    (φ₁ + φ₂) * φ₃ = φ₁ * φ₃ + φ₂ * φ₃ :=
id      └┘  └┘   └┘  └┘  └┘  └┘  └┘
src                             
typ     └┘  └┘   └┘  └┘  └┘  └┘  └┘
184  ext $ λ n, by simp only [coeff_mul, add_mul, finset.sum_add_distrib, add_monoid_hom.map_add]
id   └─┘                     └───────┘  └─────┘  └────────────────────┘  └────────────────────┘
src  └─┘           └─────────┘└───────┘└┘└─────┘└┘└────────────────────┘└┘└────────────────────┘└─
typ  └─┘          └─────────┘└───────┘└┘└─────┘└┘└────────────────────┘└┘└────────────────────┘└─
doc  └─┘           └─────────┘         └┘       └┘                      └┘                      └─
txt                └─────────┘         └┘       └┘                      └┘                      └─
par                └─────────┘         └┘       └┘                      └┘                      └─
pid                    └──┘└┘         └┘       └┘                      └┘                      
st                └───────────────────────────────────────────────────────────────────────────────
185  
src  
typ  
doc  
txt  
par  
pid  
st   
186  protected lemma mul_assoc (φ₁ φ₂ φ₃ : mv_power_series σ α) :
id                                         └─────────────┘  
src                                        └─────────────┘
typ                                        └─────────────┘  
doc                                        └─────────────┘
187    (φ₁ * φ₂) * φ₃ = φ₁ * (φ₂ * φ₃) :=
id      └┘  └┘   └┘  └┘   └┘  └┘
src                          
typ     └┘  └┘   └┘  └┘   └┘  └┘
188  ext $ λ n,
id   └─┘     
src  └─┘
typ  └─┘     
doc  └─┘
189  begin
st   └─────
190    simp only [coeff_mul],
id                └───────┘
src    └─────────┘└───────┘
typ    └─────────┘└───────┘
doc    └─────────┘         
txt    └─────────┘         
par    └─────────┘         
pid        └──┘└┘         
st   ──────────────────────┘└─
191    have := @finset.sum_sigma ((σ →₀ ℕ) × (σ →₀ ℕ)) α _ _ (antidiagonal n).support
id              └──────────────┘     └┘                                  
src    └──────┘ └──────────────┘   └┘ └┘     └─┘ └───┘              └─────────
typ    └──────┘ └──────────────┘   └┘ └┘    └─┘ └───┘             └─────────
doc    └──────┘                    └┘ └┘      └─┘ └───┘              └─────────
txt    └──────┘                       └┘      └─┘ └───┘              └─────────
par    └──────┘                       └┘      └─┘ └───┘              └─────────
pid    └───┘└─┘                       └┘      └─┘ └───┘              └─────────
st   ─────────────────────────────────────────────────────────────────────────────────
192      (λ p, (antidiagonal (p.1)).support) (λ x, coeff α x.2.1 φ₁ * coeff α x.2.2 φ₂ * coeff α x.1.2 φ₃),
id              └──────────┘                                     └┘                └┘   └───┘        └┘
src  ───┘  └──┘ └──────────┘  └────────────┘  └──┘       └───┘         └───┘   └───┘  └───┘  
typ  ───┘  └──┘ └──────────┘  └────────────┘  └──┘       └───┘└┘       └───┘└┘ └───┘ └───┘└┘
doc  ───┘  └──┘               └────────────┘  └──┘       └───┘          └───┘   └───┘  └───┘  
txt  ───┘  └──┘               └────────────┘  └──┘       └───┘          └───┘          └───┘  
par  ───┘  └──┘               └────────────┘  └──┘       └───┘          └───┘          └───┘  
pid  ───┘  └──┘               └────────────┘  └──┘       └───┘          └───┘          └───┘  
st   ────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
193    convert this.symm using 1; clear this,
id             └───────┘
src    └──────┘└───────┘└──────┘  └────────┘
typ    └──────┘└───────┘└──────┘  └────────┘
doc    └──────┘         └──────┘  └────────┘
txt    └──────┘         └──────┘  └────────┘
par    └──────┘         └──────┘  └────────┘
pid                    └─────┘       └───┘
st   ──────────────────────────────────────┘└─
194    { apply finset.sum_congr rfl,
id             └──────────────┘ └─┘
src      └────┘└──────────────┘└─┘
typ      └────┘└──────────────┘└─┘
doc      └────┘                
txt      └────┘                
par      └────┘                
pid                           
st   ───┘└────────────────────────┘└─
195      intros p hp, exact finset.sum_mul },
id                          └────────────┘
src      └─────────┘  └────┘└────────────┘
typ      └─────────┘  └────┘└────────────┘
doc      └─────────┘  └────┘              
txt      └─────────┘  └────┘              
par      └─────────┘  └────┘              
pid            └───┘                     
st   ──────────────┘└─────────────────────┘└┘
196    have := @finset.sum_sigma ((σ →₀ ℕ) × (σ →₀ ℕ)) α _ _ (antidiagonal n).support
id              └──────────────┘                                          
src    └──────┘ └──────────────┘      └┘      └─┘ └───┘              └─────────
typ    └──────┘ └──────────────┘      └┘     └─┘ └───┘             └─────────
doc    └──────┘                       └┘      └─┘ └───┘              └─────────
txt    └──────┘                       └┘      └─┘ └───┘              └─────────
par    └──────┘                       └┘      └─┘ └───┘              └─────────
pid    └───┘└─┘                       └┘      └─┘ └───┘              └─────────
st   ─────────────────────────────────────────────────────────────────────────────────
197      (λ p, (antidiagonal (p.2)).support) (λ x, coeff α x.1.1 φ₁ * (coeff α x.2.1 φ₂ * coeff α x.2.2 φ₃)),
id              └──────────┘                                     └┘                  └┘   └───┘        └┘
src  ───┘  └──┘ └──────────┘  └────────────┘  └──┘       └───┘           └───┘   └───┘  └───┘  └┘
typ  ───┘  └──┘ └──────────┘  └────────────┘  └──┘       └───┘└┘         └───┘└┘ └───┘ └───┘└┘└┘
doc  ───┘  └──┘               └────────────┘  └──┘       └───┘           └───┘   └───┘  └───┘  └┘
txt  ───┘  └──┘               └────────────┘  └──┘       └───┘           └───┘          └───┘  └┘
par  ───┘  └──┘               └────────────┘  └──┘       └───┘           └───┘          └───┘  └┘
pid  ───┘  └──┘               └────────────┘  └──┘       └───┘           └───┘          └───┘  └┘
st   ──────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
198    convert this.symm using 1; clear this,
id             └───────┘
src    └──────┘└───────┘└──────┘  └────────┘
typ    └──────┘└───────┘└──────┘  └────────┘
doc    └──────┘         └──────┘  └────────┘
txt    └──────┘         └──────┘  └────────┘
par    └──────┘         └──────┘  └────────┘
pid                    └─────┘       └───┘
st   ──────────────────────────────────────┘└─
199    { apply finset.sum_congr rfl, intros p hp, rw finset.mul_sum },
id             └──────────────┘ └─┘                  └────────────┘
src      └────┘└──────────────┘└─┘  └─────────┘  └─┘└────────────┘
typ      └────┘└──────────────┘└─┘  └─────────┘  └─┘└────────────┘
doc      └────┘                     └─────────┘  └─┘              
txt      └────┘                     └─────────┘  └─┘              
par      └────┘                     └─────────┘  └─┘              
pid                                      └───┘                  
st   ───┘└────────────────────────┘└───────────┘└──────────────────┘└┘
200    apply finset.sum_bij,
id           └────────────┘
src    └────┘└────────────┘
typ    └────┘└────────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ─────────────────────┘└─
201    swap 5,
src    └────┘
typ    └────┘
doc    └────┘
txt    └────┘
par    └────┘
pid        
st   ───────┘└─
202    { rintros ⟨⟨i,j⟩, ⟨k,l⟩⟩ H, exact ⟨(k, l+j), (l, j)⟩ },
id                                                  
src      └──────────────────────┘  └────┘  └┘  └─┘  └┘ └─┘
typ      └──────────────────────┘  └────┘ └┘  └─┘ └┘└─┘
doc      └──────────────────────┘  └────┘   └┘   └─┘  └┘ └─┘
txt      └──────────────────────┘  └────┘   └┘   └─┘  └┘ └─┘
par      └──────────────────────┘  └────┘   └┘   └─┘  └┘ └─┘
pid             └───────────────┘          └┘   └─┘  └┘ └┘
st   ───┘└──────────────────────┘└─────────────────────────┘└┘
203    { rintros ⟨⟨i,j⟩, ⟨k,l⟩⟩ H,
src      └──────────────────────┘
typ      └──────────────────────┘
doc      └──────────────────────┘
txt      └──────────────────────┘
par      └──────────────────────┘
pid             └───────────────┘
st   ───┘└──────────────────────┘└─
204      simp only [finset.mem_sigma, mem_antidiagonal_support] at H ⊢, finish },
id                  └──────────────┘  └──────────────────────┘
src      └─────────┘└──────────────┘└┘└──────────────────────┘└──────┘  └─────┘
typ      └─────────┘└──────────────┘└┘└──────────────────────┘└──────┘  └─────┘
doc      └─────────┘                └┘                        └──────┘  └─────┘
txt      └─────────┘                └┘                        └──────┘  └─────┘
par      └─────────┘                └┘                        └──────┘  └─────┘
pid          └──┘└┘                └┘                        └────┘        
st   ────────────────────────────────────────────────────────────────┘└───────┘└┘
205    { rintros ⟨⟨i,j⟩, ⟨k,l⟩⟩ H, rw mul_assoc },
id                                    └───────┘
src      └──────────────────────┘  └─┘└───────┘
typ      └──────────────────────┘  └─┘└───────┘
doc      └──────────────────────┘  └─┘         
txt      └──────────────────────┘  └─┘         
par      └──────────────────────┘  └─┘         
pid             └───────────────┘             
st   ───┘└──────────────────────┘└─────────────┘└┘
206    { rintros ⟨⟨a,b⟩, ⟨c,d⟩⟩ ⟨⟨i,j⟩, ⟨k,l⟩⟩ H₁ H₂,
src      └─────────────────────────────────────────┘
typ      └─────────────────────────────────────────┘
doc      └─────────────────────────────────────────┘
txt      └─────────────────────────────────────────┘
par      └─────────────────────────────────────────┘
pid             └──────────────────────────────────┘
st   ───┘└─────────────────────────────────────────┘└─
207      simp only [finset.mem_sigma, mem_antidiagonal_support,
id                  └──────────────┘  └──────────────────────┘
src      └─────────┘└──────────────┘└┘└──────────────────────┘└─
typ      └─────────┘└──────────────┘└┘└──────────────────────┘└─
doc      └─────────┘                └┘                        └─
txt      └─────────┘                └┘                        └─
par      └─────────┘                └┘                        └─
pid          └──┘└┘                └┘                        └─
st   ───────────────────────────────────────────────────────────
208        and_imp, prod.mk.inj_iff, add_comm, heq_iff_eq] at H₁ H₂ ⊢,
id         └─────┘  └─────────────┘  └──────┘  └────────┘
src  ─────┘└─────┘└┘└─────────────┘└┘└──────┘└┘└────────┘└──────────┘
typ  ─────┘└─────┘└┘└─────────────┘└┘└──────┘└┘└────────┘└──────────┘
doc  ─────┘       └┘               └┘        └┘          └──────────┘
txt  ─────┘       └┘               └┘        └┘          └──────────┘
par  ─────┘       └┘               └┘        └┘          └──────────┘
pid  ─────┘       └┘               └┘        └┘          └────────┘
st   ───────────────────────────────────────────────────────────────┘└─
209      finish },
src      └─────┘
typ      └─────┘
doc      └─────┘
txt      └─────┘
par      └─────┘
pid            
st   ──────────┘└┘
210    { rintros ⟨⟨i,j⟩, ⟨k,l⟩⟩ H, refine ⟨⟨(i+k, l), (i, k)⟩, _, _⟩;
id                                                      
src      └──────────────────────┘  └─────┘      └┘ └─┘  └┘ └───────┘
typ      └──────────────────────┘  └─────┘      └┘└─┘ └┘└───────┘
doc      └──────────────────────┘  └─────┘      └┘ └─┘  └┘ └───────┘
txt      └──────────────────────┘  └─────┘      └┘ └─┘  └┘ └───────┘
par      └──────────────────────┘  └─────┘      └┘ └─┘  └┘ └───────┘
pid             └───────────────┘              └┘ └─┘  └┘ └───────┘
st   ───────────────────────────┘└────────────────────────────────────
211      { simp only [finset.mem_sigma, mem_antidiagonal_support] at H ⊢, finish } }
id                    └──────────────┘  └──────────────────────┘
src        └─────────┘└──────────────┘└┘└──────────────────────┘└──────┘  └─────┘
typ        └─────────┘└──────────────┘└┘└──────────────────────┘└──────┘  └─────┘
doc        └─────────┘                └┘                        └──────┘  └─────┘
txt        └─────────┘                └┘                        └──────┘  └─────┘
par        └─────────┘                └┘                        └──────┘  └─────┘
pid            └──┘└┘                └┘                        └────┘        
st   ───┘└─────────────────────────────────────────────────────────────┘└───────┘└───
212  end
st   ──┘
213  
214  instance : semiring (mv_power_series σ α) :=
id              └──────┘  └─────────────┘  
src             └──────┘  └─────────────┘
typ             └──────┘  └─────────────┘  
doc                       └─────────────┘
215  { mul_one := mv_power_series.mul_one,
id                └─────────────────────┘
src               └─────────────────────┘
typ               └─────────────────────┘
216    one_mul := mv_power_series.one_mul,
id                └─────────────────────┘
src               └─────────────────────┘
typ               └─────────────────────┘
217    mul_assoc := mv_power_series.mul_assoc,
id                  └───────────────────────┘
src                 └───────────────────────┘
typ                 └───────────────────────┘
218    mul_zero := mv_power_series.mul_zero,
id                 └──────────────────────┘
src                └──────────────────────┘
typ                └──────────────────────┘
219    zero_mul := mv_power_series.zero_mul,
id                 └──────────────────────┘
src                └──────────────────────┘
typ                └──────────────────────┘
220    left_distrib := mv_power_series.mul_add,
id                     └─────────────────────┘
src                    └─────────────────────┘
typ                    └─────────────────────┘
221    right_distrib := mv_power_series.add_mul,
id                      └─────────────────────┘
src                     └─────────────────────┘
typ                     └─────────────────────┘
222    .. mv_power_series.has_one,
id        └─────────────────────┘
src       └─────────────────────┘
typ       └─────────────────────┘
223    .. mv_power_series.has_mul,
id        └─────────────────────┘
src       └─────────────────────┘
typ       └─────────────────────┘
224    .. mv_power_series.add_comm_monoid }
id        └─────────────────────────────┘
src       └─────────────────────────────┘
typ       └─────────────────────────────┘
225  
226  end semiring
227  
228  instance [comm_semiring α] : comm_semiring (mv_power_series σ α) :=
id             └───────────┘     └───────────┘  └─────────────┘  
src            └───────────┘      └───────────┘  └─────────────┘
typ            └───────────┘     └───────────┘  └─────────────┘  
doc                                              └─────────────┘
229  { mul_comm := λ φ ψ, ext $ λ n, finset.sum_bij (λ p hp, p.swap)
id                      └─┘       └────────────┘     └┘  └───┘
src                       └─┘        └────────────┘           └───┘
typ                     └─┘       └────────────┘     └┘  └───┘
doc                       └─┘                                 └───┘
230      (λ p hp, swap_mem_antidiagonal_support hp)
id           └┘  └───────────────────────────┘ └┘
src               └───────────────────────────┘
typ          └┘  └───────────────────────────┘ └┘
231      (λ p hp, mul_comm _ _)
id           └┘  └──────┘
src               └──────┘
typ          └┘  └──────┘
232      (λ p q hp hq H, by simpa using congr_arg prod.swap H)
id            └┘ └┘                  └───────┘ └───────┘ 
src                         └──────────┘└───────┘└───────┘
typ           └┘ └┘      └──────────┘└───────┘└───────┘
doc                         └──────────┘         └───────┘
txt                         └──────────┘                  
par                         └──────────┘                  
pid                              └────┘                  
st                         └────────────────────────────────┘
233      (λ p hp, ⟨p.swap, swap_mem_antidiagonal_support hp, p.swap_swap.symm⟩),
id           └┘   └───┘  └───────────────────────────┘ └┘  └────────┘└───┘
src                 └───┘  └───────────────────────────┘      └────────┘└───┘
typ          └┘   └───┘  └───────────────────────────┘ └┘  └────────┘└───┘
doc                 └───┘
234    .. mv_power_series.semiring }
id        └──────────────────────┘
src       └──────────────────────┘
typ       └──────────────────────┘
235  
236  instance [ring α] : ring (mv_power_series σ α) :=
id             └──┘     └──┘  └─────────────┘  
src            └──┘      └──┘  └─────────────┘
typ            └──┘     └──┘  └─────────────┘  
doc                            └─────────────┘
237  { .. mv_power_series.semiring,
id        └──────────────────────┘
src       └──────────────────────┘
typ       └──────────────────────┘
238    .. mv_power_series.add_comm_group }
id        └────────────────────────────┘
src       └────────────────────────────┘
typ       └────────────────────────────┘
239  
240  instance [comm_ring α] : comm_ring (mv_power_series σ α) :=
id             └───────┘     └───────┘  └─────────────┘  
src            └───────┘      └───────┘  └─────────────┘
typ            └───────┘     └───────┘  └─────────────┘  
doc                                      └─────────────┘
241  { .. mv_power_series.comm_semiring,
id        └───────────────────────────┘
src       └───────────────────────────┘
typ       └───────────────────────────┘
242    .. mv_power_series.add_comm_group }
id        └────────────────────────────┘
src       └────────────────────────────┘
typ       └────────────────────────────┘
243  
244  section semiring
245  variables [semiring α]
id              └──────┘
src             └──────┘
typ             └──────┘
246  
247  lemma monomial_mul_monomial (m n : σ →₀ ℕ) (a b : α) :
id                                       └┘          
src                                       └┘ 
typ                                      └┘          
doc                                       └┘
248    monomial α m a * monomial α n b = monomial α (m + n) (a * b) :=
id     └──────┘     └──────┘     └──────┘          
src    └──────┘        └──────┘        └──────┘             
typ    └──────┘     └──────┘     └──────┘          
doc    └──────┘         └──────┘         └──────┘
249  begin
st   └─────
250    ext k, rw [coeff_mul, coeff_monomial], split_ifs with h,
id                └───────┘  └────────────┘
src    └───┘  └──┘└───────┘└┘└────────────┘  └──────────────┘
typ    └───┘  └──┘└───────┘└┘└────────────┘  └──────────────┘
doc    └───┘  └──┘         └┘                └──────────────┘
txt    └───┘  └──┘         └┘                └──────────────┘
par    └───┘  └──┘         └┘                └──────────────┘
pid       └┘    └┘         └┘                         └────┘
st   ──────┘└─────────────┘└──────────────┘└─────────────────┘└─
251    { rw [h, finset.sum_eq_single (m,n)],
id             └──────────────────┘  
src      └──┘ └┘└──────────────────┘  └┘
typ      └──┘└┘└──────────────────┘└┘
doc      └──┘ └┘                       └┘
txt      └──┘ └┘                       └┘
par      └──┘ └┘                       └┘
pid        └┘ └┘                       └┘
st   ───┘└───┘└──────────────────────────┘└──
252      { rw [coeff_monomial', coeff_monomial'] },
id             └─────────────┘  └─────────────┘
src        └──┘└─────────────┘└┘└─────────────┘└┘
typ        └──┘└─────────────┘└┘└─────────────┘└┘
doc        └──┘               └┘               └┘
txt        └──┘               └┘               └┘
par        └──┘               └┘               └┘
pid          └┘               └┘               
st   ─────┘└─────────────────┘└───────────────┘└┘
253      { rintros ⟨i,j⟩ hij hne,
src        └───────────────────┘
typ        └───────────────────┘
doc        └───────────────────┘
txt        └───────────────────┘
par        └───────────────────┘
pid               └────────────┘
st   ─────┘└───────────────────┘└─
254        rw [ne.def, prod.mk.inj_iff, not_and] at hne,
id             └────┘  └─────────────┘  └─────┘
src        └──┘└────┘└┘└─────────────┘└┘└─────┘└──────┘
typ        └──┘└────┘└┘└─────────────┘└┘└─────┘└──────┘
doc        └──┘      └┘               └┘       └──────┘
txt        └──┘      └┘               └┘       └──────┘
par        └──┘      └┘               └┘       └──────┘
pid          └┘      └┘               └┘       └─────┘
st   ───────────────┘└───────────────┘└───────┘└─────┘└─
255        by_cases H : i = m,
id                        
src        └───────┘ └─┘ 
typ        └───────┘ └─┘
doc        └───────┘ └─┘  
txt        └───────┘ └─┘  
par        └───────┘ └─┘  
pid                 └─┘  
st   ───────────────────────┘└─
256        { rw [coeff_monomial j n b, if_neg (hne H), mul_zero] },
id               └────────────┘     └────┘  └─┘    └──────┘
src          └──┘└────────────┘   └┘└────┘     └─┘└──────┘└┘
typ          └──┘└────────────┘└┘└────┘ └─┘└─┘└──────┘└┘
doc          └──┘                 └┘           └─┘        └┘
txt          └──┘                 └┘           └─┘        └┘
par          └──┘                 └┘           └─┘        └┘
pid            └┘                 └┘           └─┘        
st   ───────┘└──────────────────────┘└──────────────┘└────────┘└┘
257        { rw [coeff_monomial, if_neg H, zero_mul] } },
id               └────────────┘  └────┘   └──────┘
src          └──┘└────────────┘└┘└────┘ └┘└──────┘└┘
typ          └──┘└────────────┘└┘└────┘└┘└──────┘└┘
doc          └──┘              └┘       └┘        └┘
txt          └──┘              └┘       └┘        └┘
par          └──┘              └┘       └┘        └┘
pid            └┘              └┘       └┘        
st   ─────────────────────────┘└────────┘└────────┘└──┘
258      { intro H, rw finsupp.mem_antidiagonal_support at H,
id                     └──────────────────────────────┘
src        └─────┘  └─┘└──────────────────────────────┘└───┘
typ        └─────┘  └─┘└──────────────────────────────┘└───┘
doc        └─────┘  └─┘                                └───┘
txt        └─────┘  └─┘                                └───┘
par        └─────┘  └─┘                                └───┘
pid             └┘                                    └───┘
st   ────────────┘└────────────────────────────────────────┘└─
259        exfalso, exact H rfl } },
id                         └─┘
src        └─────┘  └────┘ └─┘
typ        └─────┘  └────┘└─┘
doc        └─────┘  └────┘    
txt        └─────┘  └────┘    
par        └─────┘  └────┘    
pid                          
st   ────────────┘└────────────┘└──┘
260    { rw [finset.sum_eq_zero], rintros ⟨i,j⟩ hij,
id           └────────────────┘
src      └──┘└────────────────┘  └───────────────┘
typ      └──┘└────────────────┘  └───────────────┘
doc      └──┘                    └───────────────┘
txt      └──┘                    └───────────────┘
par      └──┘                    └───────────────┘
pid        └┘                           └────────┘
st   ─────────────────────────┘└──────────────────┘└─
261      rw finsupp.mem_antidiagonal_support at hij,
id          └──────────────────────────────┘
src      └─┘└──────────────────────────────┘└─────┘
typ      └─┘└──────────────────────────────┘└─────┘
doc      └─┘                                └─────┘
txt      └─┘                                └─────┘
par      └─┘                                └─────┘
pid                                        └─────┘
st   ─────────────────────────────────────────────┘└─
262      by_cases H : i = m,
id                       
src      └───────┘ └─┘  
typ      └───────┘ └─┘ 
doc      └───────┘ └─┘  
txt      └───────┘ └─┘  
par      └───────┘ └─┘  
pid               └─┘  
st   ─────────────────────┘└─
263      { subst i, have : j ≠ n, { rintro rfl, exact h hij.symm },
id                                                 └──────┘
src        └────┘   └─────┘      └────────┘  └────┘ └──────┘
typ        └────┘  └─────┘    └────────┘  └────┘└──────┘
doc        └────┘   └─────┘       └────────┘  └────┘         
txt        └────┘   └─────┘       └────────┘  └────┘         
par        └────┘   └─────┘       └────────┘  └────┘         
pid                └───┘└┘             └──┘                
st   ─────┘└─────┘└────────────┘└──┘└────────┘└─────────────────┘└┘
264        { rw [coeff_monomial j n b, if_neg this, mul_zero] } },
id               └────────────┘     └────┘ └──┘  └──────┘
src          └──┘└────────────┘   └┘└────┘    └┘└──────┘└┘
typ          └──┘└────────────┘└┘└────┘└──┘└┘└──────┘└┘
doc          └──┘                 └┘          └┘        └┘
txt          └──┘                 └┘          └┘        └┘
par          └──┘                 └┘          └┘        └┘
pid            └┘                 └┘          └┘        
st   ───────────────────────────────┘└───────────┘└────────┘└──┘
265      { rw [coeff_monomial, if_neg H, zero_mul] } }
id             └────────────┘  └────┘   └──────┘
src        └──┘└────────────┘└┘└────┘ └┘└──────┘└┘
typ        └──┘└────────────┘└┘└────┘└┘└──────┘└┘
doc        └──┘              └┘       └┘        └┘
txt        └──┘              └┘       └┘        └┘
par        └──┘              └┘       └┘        └┘
pid          └┘              └┘       └┘        
st   ───────────────────────┘└────────┘└────────┘└───
266  end
st   ──┘
267  
268  variables (σ) (α)
269  
270  /-- The constant multivariate formal power series.-/
271  def C : α →+* mv_power_series σ α :=
id            └─┘ └─────────────┘  
src            └─┘ └─────────────┘
typ           └─┘ └─────────────┘  
doc            └─┘ └─────────────┘
272  { map_one' := rfl,
id                 └─┘
src                └─┘
typ                └─┘
273    map_mul' := λ a b, (monomial_mul_monomial 0 0 a b).symm,
id                       └───────────────────┘       └──┘
src                        └───────────────────┘         └──┘
typ                      └───────────────────┘       └──┘
274    .. monomial α (0 : σ →₀ ℕ) }
id        └──────┘        └┘ 
src       └──────┘          └┘ 
typ       └──────┘        └┘ 
doc       └──────┘          └┘
275  
276  variables {σ} {α}
277  
278  @[simp] lemma monomial_zero_eq_C : monomial α (0 : σ →₀ ℕ) = C σ α := rfl
id                                      └──────┘        └┘          └─┘
src                                     └──────┘          └┘            └─┘
typ                                     └──────┘        └┘          └─┘
doc    └──┘                             └──────┘          └┘      
279  
280  @[simp] lemma monomial_zero_eq_C_apply (a : α) : monomial α (0 : σ →₀ ℕ) a = C σ α a := rfl
id                                                   └──────┘        └┘            └─┘
src                                                   └──────┘          └┘                └─┘
typ                                                  └──────┘        └┘            └─┘
doc    └──┘                                           └──────┘          └┘        
281  
282  lemma coeff_C (n : σ →₀ ℕ) (a : α) :
id                       └┘        
src                       └┘ 
typ                      └┘        
doc                       └┘
283    coeff α n (C σ α a) = if n = 0 then a else 0 := rfl
id     └───┘                                 └─┘
src    └───┘                                        └─┘
typ    └───┘                                 └─┘
doc    └───┘      
284  
285  @[simp] lemma coeff_zero_C (a : α) : coeff α (0 : σ →₀ℕ) (C σ α a) = a :=
id                                       └───┘        └┘         
src                                       └───┘          └┘           
typ                                      └───┘        └┘         
doc    └──┘                               └───┘          └┘    
286  coeff_monomial' 0 a
id   └─────────────┘   
src  └─────────────┘
typ  └─────────────┘   
287  
288  /-- The variables of the multivariate formal power series ring.-/
289  def X (s : σ) : mv_power_series σ α := monomial α (single s 1) 1
id                  └─────────────┘      └──────┘   └────┘ 
src                  └─────────────┘        └──────┘    └────┘
typ                 └─────────────┘      └──────┘   └────┘ 
doc                  └─────────────┘        └──────┘    └────┘
290  
291  lemma coeff_X (n : σ →₀ ℕ) (s : σ) :
id                       └┘        
src                       └┘ 
typ                      └┘        
doc                       └┘
292    coeff α n (X s : mv_power_series σ α) = if n = (single s 1) then 1 else 0 := rfl
id     └───┘        └─────────────┘           └────┘                      └─┘
src    └───┘           └─────────────┘              └────┘                       └─┘
typ    └───┘        └─────────────┘           └────┘                      └─┘
doc    └───┘           └─────────────┘                └────┘
293  
294  lemma coeff_index_single_X (s t : σ) :
id                                     
typ                                    
295    coeff α (single t 1) (X s : mv_power_series σ α) = if t = s then 1 else 0 :=
id     └───┘   └────┘          └─────────────┘          
src    └───┘    └────┘            └─────────────┘            
typ    └───┘   └────┘          └─────────────┘          
doc    └───┘    └────┘            └─────────────┘
296  by { simp only [coeff_X, single_right_inj one_ne_zero], split_ifs; refl }
id                   └─────┘  └──────────────┘ └─────────┘
src       └─────────┘└─────┘└┘└──────────────┘└─────────┘  └───────┘  └───┘
typ       └─────────┘└─────┘└┘└──────────────┘└─────────┘  └───────┘  └───┘
doc       └─────────┘       └┘                             └───────┘  └───┘
txt       └─────────┘       └┘                             └───────┘  └───┘
par       └─────────┘       └┘                             └───────┘  └───┘
pid           └──┘└┘       └┘                                            
st     └──────────────────────────────────────────────────┘└────────────────┘└┘
297  
298  @[simp] lemma coeff_index_single_self_X (s : σ) :
id                                                
typ                                               
doc    └──┘
299    coeff α (single s 1) (X s : mv_power_series σ α) = 1 :=
id     └───┘   └────┘          └─────────────┘    
src    └───┘    └────┘            └─────────────┘      
typ    └───┘   └────┘          └─────────────┘    
doc    └───┘    └────┘            └─────────────┘
300  if_pos rfl
id   └────┘ └─┘
src  └────┘ └─┘
typ  └────┘ └─┘
301  
302  @[simp] lemma coeff_zero_X (s : σ) : coeff α (0 : σ →₀ ℕ) (X s : mv_power_series σ α) = 0 :=
id                                       └───┘        └┘        └─────────────┘    
src                                       └───┘          └┘         └─────────────┘      
typ                                      └───┘        └┘        └─────────────┘    
doc    └──┘                               └───┘          └┘          └─────────────┘
303  by { rw [coeff_X, if_neg], intro h, exact one_ne_zero (single_eq_zero.mp h.symm) }
id            └─────┘  └────┘                  └─────────┘  └───────────────┘ └────┘
src       └──┘└─────┘└┘└────┘  └─────┘  └────┘└─────────┘ └───────────────┘└────┘└┘
typ       └──┘└─────┘└┘└────┘  └─────┘  └────┘└─────────┘ └───────────────┘└────┘└┘
doc       └──┘       └┘        └─────┘  └────┘                                   └┘
txt       └──┘       └┘        └─────┘  └────┘                                   └┘
par       └──┘       └┘        └─────┘  └────┘                                   └┘
pid         └┘       └┘             └┘                                          
st     └────────────┘└──────┘└────────┘└─────────────────────────────────────────────┘└┘
304  
305  lemma X_def (s : σ) : X s = monomial α (single s 1) 1 := rfl
id                           └──────┘   └────┘          └─┘
src                            └──────┘    └────┘           └─┘
typ                          └──────┘   └────┘          └─┘
doc                             └──────┘    └────┘
306  
307  lemma X_pow_eq (s : σ) (n : ℕ) :
id                              
src                              
typ                             
308    (X s : mv_power_series σ α)^n = monomial α (single s n) 1 :=
id          └─────────────┘     └──────┘   └────┘  
src          └─────────────┘        └──────┘    └────┘
typ         └─────────────┘     └──────┘   └────┘  
doc          └─────────────┘          └──────┘    └────┘
309  begin
st   └─────
310    induction n with n ih,
id               
src    └────────┘ └────────┘
typ    └────────┘└────────┘
doc    └────────┘ └────────┘
txt    └────────┘ └────────┘
par    └────────┘ └────────┘
pid              └───────┘
st   ──────────────────────┘└─
311    { rw [pow_zero, finsupp.single_zero], refl },
id           └──────┘  └─────────────────┘
src      └──┘└──────┘└┘└─────────────────┘  └───┘
typ      └──┘└──────┘└┘└─────────────────┘  └───┘
doc      └──┘        └┘                     └───┘
txt      └──┘        └┘                     └───┘
par      └──┘        └┘                     └───┘
pid        └┘        └┘                         
st   ───┘└──────────┘└───────────────────┘└─────┘└┘
312    { rw [pow_succ', ih, nat.succ_eq_add_one, finsupp.single_add, X, monomial_mul_monomial, one_mul] }
id           └───────┘  └┘  └─────────────────┘  └────────────────┘    └───────────────────┘  └─────┘
src      └──┘└───────┘└┘  └┘└─────────────────┘└┘└────────────────┘└┘└┘└───────────────────┘└┘└─────┘└┘
typ      └──┘└───────┘└┘└┘└┘└─────────────────┘└┘└────────────────┘└┘└┘└───────────────────┘└┘└─────┘└┘
doc      └──┘         └┘  └┘                   └┘                  └┘└┘                     └┘       └┘
txt      └──┘         └┘  └┘                   └┘                  └┘ └┘                     └┘       └┘
par      └──┘         └┘  └┘                   └┘                  └┘ └┘                     └┘       └┘
pid        └┘         └┘  └┘                   └┘                  └┘ └┘                     └┘       
st   ────────────────┘└──┘└───────────────────┘└──────────────────┘└─┘└─────────────────────┘└───────┘└─
313  end
st   ──┘
314  
315  lemma coeff_X_pow (m : σ →₀ ℕ) (s : σ) (n : ℕ) :
id                           └┘               
src                           └┘                
typ                          └┘               
doc                           └┘
316    coeff α m ((X s : mv_power_series σ α)^n) = if m = single s n then 1 else 0 :=
id     └───┘         └─────────────┘           └────┘  
src    └───┘            └─────────────┘               └────┘
typ    └───┘         └─────────────┘           └────┘  
doc    └───┘            └─────────────┘                  └────┘
317  by rw [X_pow_eq s n, coeff_monomial]
id          └──────┘    └────────────┘
src     └──┘└──────┘  └┘└────────────┘└─
typ     └──┘└──────┘└┘└────────────┘└─
doc     └──┘          └┘              └─
txt     └──┘          └┘              └─
par     └──┘          └┘              └─
pid       └┘          └┘              
st     └───────────────┘└──────────────┘
318  
src  
typ  
doc  
txt  
par  
pid  
st   
319  @[simp] lemma coeff_mul_C (n : σ →₀ ℕ) (φ : mv_power_series σ α) (a : α) :
id                                   └┘        └─────────────┘         
src                                   └┘        └─────────────┘
typ                                  └┘        └─────────────┘         
doc    └──┘                           └┘         └─────────────┘
320    coeff α n (φ * (C σ α a)) = (coeff α n φ) * a :=
id     └───┘               └───┘      
src    └───┘                     └───┘        
typ    └───┘               └───┘      
doc    └───┘                       └───┘
321  begin
st   └─────
322    rw [coeff_mul n φ], rw [finset.sum_eq_single (n,(0 : σ →₀ ℕ))],
id         └───────┘         └──────────────────┘        └┘
src    └──┘└───────┘    └──┘└──────────────────┘  └──┘ └┘ └─┘
typ    └──┘└───────┘  └──┘└──────────────────┘ └──┘└┘ └─┘
doc    └──┘             └──┘                       └──┘ └┘ └─┘
txt    └──┘             └──┘                       └──┘    └─┘
par    └──┘             └──┘                       └──┘    └─┘
pid      └┘               └┘                       └──┘    └─┘
st   ──────────────────┘└──────────────────────────────────────────┘└──
323    { rw [coeff_C, if_pos rfl] },
id           └─────┘  └────┘ └─┘
src      └──┘└─────┘└┘└────┘└─┘└┘
typ      └──┘└─────┘└┘└────┘└─┘└┘
doc      └──┘       └┘         └┘
txt      └──┘       └┘         └┘
par      └──┘       └┘         └┘
pid        └┘       └┘         
st   ───┘└─────────┘└──────────┘└┘
324    { rintro ⟨i,j⟩ hij hne,
src      └──────────────────┘
typ      └──────────────────┘
doc      └──────────────────┘
txt      └──────────────────┘
par      └──────────────────┘
pid            └────────────┘
st   ───┘└──────────────────┘└─
325      rw finsupp.mem_antidiagonal_support at hij,
id          └──────────────────────────────┘
src      └─┘└──────────────────────────────┘└─────┘
typ      └─┘└──────────────────────────────┘└─────┘
doc      └─┘                                └─────┘
txt      └─┘                                └─────┘
par      └─┘                                └─────┘
pid                                        └─────┘
st   ─────────────────────────────────────────────┘└─
326      by_cases hj : j = 0,
id                      
src      └───────┘  └─┘ └┘
typ      └───────┘  └─┘└┘
doc      └───────┘  └─┘  └┘
txt      └───────┘  └─┘  └┘
par      └───────┘  └─┘  └┘
pid                └─┘  
st   ──────────────────────┘└─
327      { subst hj, simp at *, contradiction },
id               └┘
src        └────┘    └───────┘  └────────────┘
typ        └────┘└┘  └───────┘  └────────────┘
doc        └────┘    └───────┘  └────────────┘
txt        └────┘    └───────┘  └────────────┘
par        └────┘    └───────┘  └────────────┘
pid                     └──┘               
st   ─────┘└──────┘└─────────┘└──────────────┘└┘
328      { rw [coeff_C, if_neg hj, mul_zero] } },
id             └─────┘  └────┘ └┘  └──────┘
src        └──┘└─────┘└┘└────┘  └┘└──────┘└┘
typ        └──┘└─────┘└┘└────┘└┘└┘└──────┘└┘
doc        └──┘       └┘        └┘        └┘
txt        └──┘       └┘        └┘        └┘
par        └──┘       └┘        └┘        └┘
pid          └┘       └┘        └┘        
st   ────────────────┘└─────────┘└────────┘└──┘
329    { intro h, exfalso, apply h,
src      └─────┘  └─────┘  └────┘
typ      └─────┘  └─────┘  └────┘
doc      └─────┘  └─────┘  └────┘
txt      └─────┘  └─────┘  └────┘
par      └─────┘  └─────┘  └────┘
pid           └┘                
st   ──────────┘└───────┘└───────┘└─
330      rw finsupp.mem_antidiagonal_support,
id          └──────────────────────────────┘
src      └─┘└──────────────────────────────┘
typ      └─┘└──────────────────────────────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ──────────────────────────────────────┘└─
331      apply add_zero }
id             └──────┘
src      └────┘└──────┘
typ      └────┘└──────┘
doc      └────┘        
txt      └────┘        
par      └────┘        
pid                   
st   ──────────────────┘└─
332  end
st   ──┘
333  
334  @[simp] lemma coeff_zero_mul_X (φ : mv_power_series σ α) (s : σ) :
id                                       └─────────────┘         
src                                      └─────────────┘
typ                                      └─────────────┘         
doc    └──┘                              └─────────────┘
335    coeff α (0 : σ →₀ ℕ) (φ * X s) = 0 :=
id     └───┘        └┘         
src    └───┘          └┘           
typ    └───┘        └┘         
doc    └───┘          └┘         
336  begin
st   └─────
337    rw [coeff_mul _ φ, finset.sum_eq_zero],
id         └───────┘     └────────────────┘
src    └──┘└───────┘└─┘ └┘└────────────────┘
typ    └──┘└───────┘└─┘└┘└────────────────┘
doc    └──┘         └─┘ └┘                  
txt    └──┘         └─┘ └┘                  
par    └──┘         └─┘ └┘                  
pid      └┘         └─┘ └┘                  
st   ──────────────────┘└──────────────────┘└──
338    rintro ⟨i,j⟩ hij,
src    └──────────────┘
typ    └──────────────┘
doc    └──────────────┘
txt    └──────────────┘
par    └──────────────┘
pid          └────────┘
st   ─────────────────┘└─
339    obtain ⟨rfl, rfl⟩ : i = 0 ∧ j = 0,
id                              
src    └──────────────────┘ └─┘  └┘
typ    └──────────────────┘└─┘ └┘
doc    └──────────────────┘  └─┘   └┘
txt    └──────────────────┘  └─┘   └┘
par    └──────────────────┘  └─┘   └┘
pid          └────────────┘  └─┘   
st   ──────────────────────────────────┘└─
340    { rw finsupp.mem_antidiagonal_support at hij,
id          └──────────────────────────────┘
src      └─┘└──────────────────────────────┘└─────┘
typ      └─┘└──────────────────────────────┘└─────┘
doc      └─┘                                └─────┘
txt      └─┘                                └─────┘
par      └─┘                                └─────┘
pid                                        └─────┘
st   ───┘└────────────────────────────────────────┘└─
341      simpa using hij },
id                   └─┘
src      └──────────┘   
typ      └──────────┘└─┘
doc      └──────────┘   
txt      └──────────┘   
par      └──────────┘   
pid           └────┘   
st   ───────────────────┘└┘
342    simp,
src    └──┘
typ    └──┘
doc    └──┘
txt    └──┘
par    └──┘
st   ─────┘└─
343  end
st   ──┘
344  
345  variables (σ) (α)
346  
347  /-- The constant coefficient of a formal power series.-/
348  def constant_coeff : (mv_power_series σ α) →+* α :=
id                         └─────────────┘    └─┘ 
src                        └─────────────┘      └─┘
typ                        └─────────────┘    └─┘ 
doc                        └─────────────┘      └─┘
349  { to_fun := coeff α (0 : σ →₀ ℕ),
id               └───┘        └┘ 
src              └───┘          └┘ 
typ              └───┘        └┘ 
doc              └───┘          └┘
350    map_one' := coeff_zero_one,
id                 └────────────┘
src                └────────────┘
typ                └────────────┘
351    map_mul' := λ φ ψ, by simp [coeff_mul, support_single_ne_zero],
id                               └───────┘  └────────────────────┘
src                          └────┘└───────┘└┘└────────────────────┘
typ                        └────┘└───────┘└┘└────────────────────┘
doc                          └────┘         └┘                      
txt                          └────┘         └┘                      
par                          └────┘         └┘                      
pid                                       └┘                      
st                          └───────────────────────────────────────┘
352    .. coeff α (0 : σ →₀ ℕ) }
id        └───┘        └┘ 
src       └───┘          └┘ 
typ       └───┘        └┘ 
doc       └───┘          └┘
353  
354  variables {σ} {α}
355  
356  @[simp] lemma coeff_zero_eq_constant_coeff :
doc    └──┘
357    coeff α (0 : σ →₀ ℕ) = constant_coeff σ α := rfl
id     └───┘        └┘    └────────────┘      └─┘
src    └───┘          └┘    └────────────┘        └─┘
typ    └───┘        └┘    └────────────┘      └─┘
doc    └───┘          └┘      └────────────┘
358  @[simp] lemma coeff_zero_eq_constant_coeff_apply (φ : mv_power_series σ α) :
id                                                         └─────────────┘  
src                                                        └─────────────┘
typ                                                        └─────────────┘  
doc    └──┘                                                └─────────────┘
359    coeff α (0 : σ →₀ ℕ) φ = constant_coeff σ α φ := rfl
id     └───┘        └┘     └────────────┘       └─┘
src    └───┘          └┘      └────────────┘          └─┘
typ    └───┘        └┘     └────────────┘       └─┘
doc    └───┘          └┘        └────────────┘
360  
361  @[simp] lemma constant_coeff_C (a : α) : constant_coeff σ α (C σ α a) = a := rfl
id                                           └────────────┘              └─┘
src                                           └────────────┘                    └─┘
typ                                          └────────────┘              └─┘
doc    └──┘                                   └────────────┘      
362  @[simp] lemma constant_coeff_comp_C :
doc    └──┘
363    (constant_coeff σ α).comp (C σ α) = ring_hom.id α := rfl
id      └────────────┘   └──┘        └─────────┘     └─┘
src     └────────────┘     └──┘          └─────────┘      └─┘
typ     └────────────┘   └──┘        └─────────┘     └─┘
doc     └────────────┘     └──┘           └─────────┘
364  
365  @[simp] lemma constant_coeff_zero : constant_coeff σ α 0 = 0 := rfl
id                                       └────────────┘           └─┘
src                                      └────────────┘             └─┘
typ                                      └────────────┘           └─┘
doc    └──┘                              └────────────┘
366  @[simp] lemma constant_coeff_one : constant_coeff σ α 1 = 1 := rfl
id                                      └────────────┘           └─┘
src                                     └────────────┘             └─┘
typ                                     └────────────┘           └─┘
doc    └──┘                             └────────────┘
367  @[simp] lemma constant_coeff_X (s : σ) : constant_coeff σ α (X s) = 0 := coeff_zero_X s
id                                           └────────────┘             └──────────┘ 
src                                           └────────────┘                └──────────┘
typ                                          └────────────┘             └──────────┘ 
doc    └──┘                                   └────────────┘      
368  
369  /-- If a multivariate formal power series is invertible,
370   then so is its constant coefficient.-/
371  lemma is_unit_constant_coeff (φ : mv_power_series σ α) (h : is_unit φ) :
id                                     └─────────────┘         └─────┘ 
src                                    └─────────────┘           └─────┘
typ                                    └─────────────┘         └─────┘ 
doc                                    └─────────────┘           └─────┘
372    is_unit (constant_coeff σ α φ) :=
id     └─────┘  └────────────┘   
src    └─────┘  └────────────┘
typ    └─────┘  └────────────┘   
doc    └─────┘  └────────────┘
373  h.map' (constant_coeff σ α)
id   └───┘  └────────────┘  
src   └───┘  └────────────┘
typ  └───┘  └────────────┘  
doc          └────────────┘
374  
375  instance : semimodule α (mv_power_series σ α) :=
id              └────────┘   └─────────────┘  
src             └────────┘    └─────────────┘
typ             └────────┘   └─────────────┘  
doc             └────────┘    └─────────────┘
376  { smul := λ a φ, C σ α a * φ,
id                       
src                          
typ                      
doc                   
377    one_smul := λ φ, one_mul _,
id                     └─────┘
src                     └─────┘
typ                    └─────┘
378    mul_smul := λ a b φ, by simp [ring_hom.map_mul, mul_assoc],
id                                └──────────────┘  └───────┘
src                            └────┘└──────────────┘└┘└───────┘
typ                         └────┘└──────────────┘└┘└───────┘
doc                            └────┘└──────────────┘└┘         
txt                            └────┘                └┘         
par                            └────┘                └┘         
pid                                                └┘         
st                            └─────────────────────────────────┘
379    smul_add := λ a φ ψ, mul_add _ _ _,
id                       └─────┘
src                         └─────┘
typ                      └─────┘
380    smul_zero := λ a, mul_zero _,
id                      └──────┘
src                      └──────┘
typ                     └──────┘
381    add_smul := λ a b φ, by simp only [ring_hom.map_add, add_mul],
id                                     └──────────────┘  └─────┘
src                            └─────────┘└──────────────┘└┘└─────┘
typ                         └─────────┘└──────────────┘└┘└─────┘
doc                            └─────────┘└──────────────┘└┘       
txt                            └─────────┘                └┘       
par                            └─────────┘                └┘       
pid                                └──┘└┘                └┘       
st                            └────────────────────────────────────┘
382    zero_smul := λ φ, by simp only [zero_mul, ring_hom.map_zero] }
id                                    └──────┘  └───────────────┘
src                         └─────────┘└──────┘└┘└───────────────┘└┘
typ                        └─────────┘└──────┘└┘└───────────────┘└┘
doc                         └─────────┘        └┘└───────────────┘└┘
txt                         └─────────┘        └┘                 └┘
par                         └─────────┘        └┘                 └┘
pid                             └──┘└┘        └┘                 
st                         └───────────────────────────────────────┘
383  
384  end semiring
385  
386  instance [ring α] : module α (mv_power_series σ α) :=
id             └──┘     └────┘   └─────────────┘  
src            └──┘      └────┘    └─────────────┘
typ            └──┘     └────┘   └─────────────┘  
doc                      └────┘    └─────────────┘
387  { ..mv_power_series.semimodule }
id       └────────────────────────┘
src      └────────────────────────┘
typ      └────────────────────────┘
388  
389  instance [comm_ring α] : algebra α (mv_power_series σ α) :=
id             └───────┘     └─────┘   └─────────────┘  
src            └───────┘      └─────┘    └─────────────┘
typ            └───────┘     └─────┘   └─────────────┘  
doc                           └─────┘    └─────────────┘
390  { to_fun := C σ α,
id                 
src              
typ                
doc              
391    commutes' := λ _ _, mul_comm _ _,
id                       └──────┘
src                        └──────┘
typ                      └──────┘
392    smul_def' := λ c p, rfl,
id                       └─┘
src                        └─┘
typ                      └─┘
393    .. mv_power_series.module }
id        └────────────────────┘
src       └────────────────────┘
typ       └────────────────────┘
394  
395  section map
396  variables {β : Type*} {γ : Type*} [semiring α] [semiring β] [semiring γ]
id                                      └──────┘     └──────┘     └──────┘
src                                     └──────┘     └──────┘     └──────┘
typ                                     └──────┘     └──────┘     └──────┘
397  variables (f : α →+* β) (g : β →+* γ)
id                    └─┘           └─┘
src                   └─┘           └─┘
typ                   └─┘           └─┘
doc                   └─┘           └─┘
398  
399  variable (σ)
400  
401  /-- The map between multivariate formal power series induced by a map on the coefficients.-/
402  def map : mv_power_series σ α →+* mv_power_series σ β :=
id             └─────────────┘   └─┘ └─────────────┘  
src            └─────────────┘     └─┘ └─────────────┘
typ            └─────────────┘   └─┘ └─────────────┘  
doc            └─────────────┘     └─┘ └─────────────┘
403  { to_fun := λ φ n, f $ coeff α n φ,
id                       └───┘   
src                         └───┘
typ                      └───┘   
doc                         └───┘
404    map_zero' := ext $ λ n, f.map_zero,
id                  └─┘       └───────┘
src                 └─┘         └───────┘
typ                 └─┘       └───────┘
doc                 └─┘         └───────┘
405    map_one' := ext $ λ n, show f ((coeff α n) 1) = (coeff β n) 1,
id                 └─┘               └───┘         └───┘  
src                └─┘                 └───┘           └───┘
typ                └─┘               └───┘         └───┘  
doc                └─┘                 └───┘            └───┘
406      by { rw [coeff_one, coeff_one], split_ifs; simp [f.map_one, f.map_zero] },
id                └───────┘  └───────┘
src           └──┘└───────┘└┘└───────┘  └───────┘  └────┘         └┘          └┘
typ           └──┘└───────┘└┘└───────┘  └───────┘  └────┘└───────┘└┘└────────┘└┘
doc           └──┘         └┘           └───────┘  └────┘         └┘          └┘
txt           └──┘         └┘           └───────┘  └────┘         └┘          └┘
par           └──┘         └┘           └───────┘  └────┘         └┘          └┘
pid             └┘         └┘                                   └┘          
st         └──────────────┘└─────────┘└─────────────────────────────────────────┘└┘
407    map_add' := λ φ ψ, ext $ λ n,
id                      └─┘     
src                       └─┘
typ                     └─┘     
doc                       └─┘
408      show f ((coeff α n) (φ + ψ)) = f ((coeff α n) φ) + f ((coeff α n) ψ), by simp,
id               └───┘              └───┘          └───┘    
src               └───┘                   └───┘              └───┘             └──┘
typ              └───┘              └───┘          └───┘          └──┘
doc               └───┘                     └───┘               └───┘             └──┘
txt                                                                               └──┘
par                                                                               └──┘
st                                                                               └───┘
409    map_mul' := λ φ ψ, ext $ λ n, show f _ = _,
id                      └─┘               
src                       └─┘                 
typ                     └─┘               
doc                       └─┘
410    begin
st     └─────
411      rw [coeff_mul, ← finset.sum_hom _ f, coeff_mul, finset.sum_congr rfl],
id           └───────┘    └────────────┘     └───────┘  └──────────────┘ └─┘
src      └──┘└───────┘└──┘└────────────┘└─┘ └┘└───────┘└┘└──────────────┘└─┘
typ      └──┘└───────┘└──┘└────────────┘└─┘└┘└───────┘└┘└──────────────┘└─┘
doc      └──┘         └──┘              └─┘ └┘         └┘                   
txt      └──┘         └──┘              └─┘ └┘         └┘                   
par      └──┘         └──┘              └─┘ └┘         └┘                   
pid        └┘         └──┘              └─┘ └┘         └┘                   
st   ────────────────┘└────────────────────┘└─────────┘└────────────────────┘└─
412      rintros ⟨i,j⟩ hij, rw [f.map_mul], refl,
src      └───────────────┘  └──┘
typ      └───────────────┘  └──┘└───────┘
doc      └───────────────┘  └──┘
txt      └───────────────┘  └──┘
par      └───────────────┘  └──┘
pid             └────────┘    └┘
st   ────────────────────┘└─────────────┘       └─
413    end }
st   ────┘
414  
415  variable {σ}
416  
417  @[simp] lemma map_id : map σ (ring_hom.id α) = ring_hom.id _ := rfl
id                          └─┘   └─────────┘    └─────────┘      └─┘
src                         └─┘    └─────────┘     └─────────┘      └─┘
typ                         └─┘   └─────────┘    └─────────┘      └─┘
doc    └──┘                 └─┘    └─────────┘      └─────────┘
418  
419  lemma map_comp : map σ (g.comp f) = (map σ g).comp (map σ f) := rfl
id                    └─┘   └───┘     └─┘   └──┘   └─┘       └─┘
src                   └─┘     └───┘      └─┘     └──┘   └─┘         └─┘
typ                   └─┘   └───┘     └─┘   └──┘   └─┘       └─┘
doc                   └─┘     └───┘       └─┘     └──┘   └─┘
420  
421  @[simp] lemma coeff_map (n : σ →₀ ℕ) (φ : mv_power_series σ α) :
id                                 └┘        └─────────────┘  
src                                 └┘        └─────────────┘
typ                                └┘        └─────────────┘  
doc    └──┘                         └┘         └─────────────┘
422    coeff β n (map σ f φ) = f (coeff α n φ) := rfl
id     └───┘    └─┘        └───┘        └─┘
src    └───┘      └─┘            └───┘           └─┘
typ    └───┘    └─┘        └───┘        └─┘
doc    └───┘      └─┘             └───┘
423  
424  @[simp] lemma constant_coeff_map (φ : mv_power_series σ α) :
id                                         └─────────────┘  
src                                        └─────────────┘
typ                                        └─────────────┘  
doc    └──┘                                └─────────────┘
425    constant_coeff σ β (map σ f φ) = f (constant_coeff σ α φ) := rfl
id     └────────────┘    └─┘        └────────────┘        └─┘
src    └────────────┘      └─┘            └────────────┘           └─┘
typ    └────────────┘    └─┘        └────────────┘        └─┘
doc    └────────────┘      └─┘             └────────────┘
426  
427  end map
428  
429  section trunc
430  variables [comm_semiring α] (n : σ →₀ ℕ)
id              └───────────┘           └┘ 
src             └───────────┘           └┘ 
typ             └───────────┘           └┘ 
doc                                     └┘
431  
432  -- Auxiliary definition for the truncation function.
433  def trunc_fun (φ : mv_power_series σ α) : mv_polynomial σ α :=
id                      └─────────────┘      └───────────┘  
src                     └─────────────┘        └───────────┘
typ                     └─────────────┘      └───────────┘  
doc                     └─────────────┘        └───────────┘
434  { support := (n.antidiagonal.support.image prod.fst).filter (λ m, coeff α m φ ≠ 0),
id                 └───────────┘└──────┘└────┘ └──────┘ └────┘       └───┘    
src                 └───────────┘└──────┘└────┘ └──────┘ └────┘        └───┘       
typ                └───────────┘└──────┘└────┘ └──────┘ └────┘       └───┘    
doc                                      └────┘          └────┘        └───┘
435    to_fun := λ m, if m ≤ n then coeff α m φ else 0,
id                              └───┘   
src                                └───┘
typ                             └───┘   
doc                                 └───┘
436    mem_support_to_fun := λ m,
id                             
typ                            
437    begin
st     └───┘
438      suffices : m ∈ finset.image prod.fst ((antidiagonal n).support) ↔ m ≤ n,
id                                                                       
src                                                                      
typ                                                                      
439      { rw [finset.mem_filter, this], split,
440        { intro h, rw [if_pos h.1], exact h.2 },
st                                               └┘
441        { intro h, split_ifs at h with H H,
442          { exact ⟨H, h⟩ },
st                          └┘
443          { exfalso, exact h rfl } } },
st                                  └────┘
444      rw finset.mem_image, split,
445      { rintros ⟨⟨i,j⟩, h, rfl⟩ s,
446        rw finsupp.mem_antidiagonal_support at h,
447        rw ← h, exact nat.le_add_right _ _ },
st                                            └┘
448      { intro h, refine ⟨(m, n-m), _, rfl⟩,
id                              
typ                             
449        rw finsupp.mem_antidiagonal_support, ext s, exact nat.add_sub_of_le (h s) }
id                                                                                
typ                                                                               
st                                                                                   └┘
450    end }
st     └─┘
451  
452  variable (α)
453  
454  /-- The `n`th truncation of a multivariate formal power series to a multivariate polynomial -/
455  def trunc : mv_power_series σ α →+ mv_polynomial σ α :=
id                                                   
typ                                                  
456  { to_fun := trunc_fun n,
id                         
typ                        
457    map_zero' := mv_polynomial.ext _ _ $ λ m, by { change ite _ _ _ = _, split_ifs; refl },
id                                                                                    └──┘
src                                                                                    └──┘
typ                                                                                   └──┘
doc                                                                                    └──┘
st                                                                                          └┘
458    map_add' := λ φ ψ, mv_polynomial.ext _ _ $ λ m,
id                                                
typ                                               
459    begin
460      rw mv_polynomial.coeff_add,
461      change ite _ _ _ = ite _ _ _ + ite _ _ _,
462      split_ifs with H, {refl}, {rw [zero_add]}
st                              └┘              └─┘
463    end }
st     └─┘
464  
465  variable {α}
466  
467  lemma coeff_trunc (m : σ →₀ ℕ) (φ : mv_power_series σ α) :
id                                                      
src                              
typ                                                     
468    mv_polynomial.coeff m (trunc α n φ) =
id                                  
typ                                 
469    if m ≤ n then coeff α m φ else 0 := rfl
id                        
typ                       
470  
471  @[simp] lemma trunc_one : trunc α n 1 = 1 :=
id                                    
typ                                   
doc    └──┘
472  mv_polynomial.ext _ _ $ λ m,
id                             
typ                            
473  begin
474    rw [coeff_trunc, coeff_one],
475    split_ifs with H H' H',
476    { subst m, erw mv_polynomial.coeff_C 0, simp },
id             
typ            
st                                                  └┘
477    { symmetry, erw mv_polynomial.coeff_monomial, convert if_neg (ne.elim (ne.symm H')), },
st                                                                                          └┘
478    { symmetry, erw mv_polynomial.coeff_monomial, convert if_neg _,
479      intro H', apply H, subst m, intro s, exact nat.zero_le _ }
id                                
typ                               
st                                                                └─
480  end
st   ──┘
481  
482  @[simp] lemma trunc_C (a : α) : trunc α n (C σ α a) = mv_polynomial.C a :=
id                                                                   
typ                                                                  
doc    └──┘
483  mv_polynomial.ext _ _ $ λ m,
id                             
typ                            
484  begin
485    rw [coeff_trunc, coeff_C, mv_polynomial.coeff_C],
486    split_ifs with H; refl <|> try {simp * at *},
id                       └──┘     └─┘
src                      └──┘     └─┘
typ                      └──┘     └─┘
doc                      └──┘     └─┘
st                                                └┘
487    exfalso, apply H, subst m, intro s, exact nat.zero_le _
id                             
typ                            
488  end
st   └─┘
489  
490  end trunc
491  
492  section comm_semiring
493  variable [comm_semiring α]
id             └┘ └───┘  └─┘
src            └┘ └───┘  └─┘
typ            └┘ └───┘  └─┘
494  
495  lemma X_pow_dvd_iff {s : σ} {n : ℕ} {φ : mv_power_series σ α} :
id                                                           
src                                   
typ                                                          
496    (X s : mv_power_series σ α)^n ∣ φ ↔ ∀ m : σ →₀ ℕ, m s < n → coeff α m φ = 0 :=
id                                                               
src                                                   
typ                                                              
497  begin
498    split,
499    { rintros ⟨φ, rfl⟩ m h,
500      rw [coeff_mul, finset.sum_eq_zero],
501      rintros ⟨i,j⟩ hij, rw [coeff_X_pow, if_neg, zero_mul],
502      contrapose! h, subst i, rw finsupp.mem_antidiagonal_support at hij,
id                            
typ                           
503      rw [← hij, finsupp.add_apply, finsupp.single_eq_same], exact nat.le_add_right n _ },
id                                                                                     
typ                                                                                    
st                                                                                         └┘
504    { intro h, refine ⟨λ m, coeff α (m + (single s n)) φ, _⟩,
id                                                    
typ                                                   
505      ext m, by_cases H : m - single s n + single s n = m,
id                                                    
typ                                                   
506      { rw [coeff_mul, finset.sum_eq_single (single s n, m - single s n)],
id                                                                     
typ                                                                    
507        { rw [coeff_X_pow, if_pos rfl, one_mul],
508          simpa using congr_arg (λ (m : σ →₀ ℕ), coeff α m φ) H.symm },
id                                                          
typ                                                         
st                                                                      └┘
509        { rintros ⟨i,j⟩ hij hne, rw finsupp.mem_antidiagonal_support at hij,
510          rw coeff_X_pow, split_ifs with hi,
511          { exfalso, apply hne, rw [← hij, ← hi, prod.mk.inj_iff], refine ⟨rfl, _⟩,
512            ext t, simp only [nat.add_sub_cancel_left, finsupp.add_apply, finsupp.nat_sub_apply] },
st                                                                                                  └┘
513          { exact zero_mul _ } },
st                              └──┘
514          { intro hni, exfalso, apply hni, rwa [finsupp.mem_antidiagonal_support, add_comm] } },
st                                                                                             └──┘
515      { rw [h, coeff_mul, finset.sum_eq_zero],
516        { rintros ⟨i,j⟩ hij, rw finsupp.mem_antidiagonal_support at hij,
517          rw coeff_X_pow, split_ifs with hi,
518          { exfalso, apply H, rw [← hij, hi], ext t,
519            simp only [nat.add_sub_cancel_left, add_comm,
520              finsupp.add_apply, add_right_inj, finsupp.nat_sub_apply] },
st                                                                        └┘
521          { exact zero_mul _ } },
st                              └──┘
522        { classical, contrapose! H, ext t,
523          by_cases hst : s = t,
id                             
typ                            
524          { subst t, simpa using nat.add_sub_cancel' H },
id                   
typ                  
st                                                        └┘
525          { simp [finsupp.single_apply, hst] } } } }
id                                         └─┘
typ                                        └─┘
st                                              └───────
526  end
st   ──┘
527  
528  lemma X_dvd_iff {s : σ} {φ : mv_power_series σ α} :
id                                                
typ                                               
529    (X s : mv_power_series σ α) ∣ φ ↔ ∀ m : σ →₀ ℕ, m s = 0 → coeff α m φ = 0 :=
id                                                               
src                                                 
typ                                                              
530  begin
531    rw [← pow_one (X s : mv_power_series σ α), X_pow_dvd_iff],
532    split; intros h m hm,
533    { exact h m (hm.symm ▸ zero_lt_one) },
id               
typ              
st                                         └┘
534    { exact h m (nat.eq_zero_of_le_zero $ nat.le_of_succ_le_succ hm) }
id               
typ              
st                                                                      └─
535  end
st   ──┘
536  end comm_semiring
537  
538  section ring
539  variables [ring α]
id              └┘ 
src             └┘ 
typ             └┘ 
540  
541  /-
542  The inverse of a multivariate formal power series is defined by
543  well-founded recursion on the coeffients of the inverse.
544  -/
545  
546  /-- Auxiliary definition that unifies
547   the totalised inverse formal power series `(_)⁻¹` and
548   the inverse formal power series that depends on
549   an inverse of the constant coefficient `inv_of_unit`.-/
550  protected noncomputable def inv.aux (a : α) (φ : mv_power_series σ α) : mv_power_series σ α
id                                                                                         
typ                                                                                        
551  | n := if n = 0 then a else
id                        
typ                       
552  - a * n.antidiagonal.support.sum (λ (x : (σ →₀ ℕ) × (σ →₀ ℕ)),
id                                                         
src                                                           
typ                                                        
553      if h : x.2 < n then coeff α x.1 φ * inv.aux x.2 else 0)
id                                           └┘
typ                                          └┘
554  using_well_founded
555  { rel_tac := λ _ _, `[exact ⟨_, finsupp.lt_wf σ⟩],
id                   
typ                  
556    dec_tac := tactic.assumption }
id                └───────────────┘
src               └───────────────┘
typ               └───────────────┘
557  
558  lemma coeff_inv_aux (n : σ →₀ ℕ) (a : α) (φ : mv_power_series σ α) :
id                                                               
src                                
typ                                                              
559    coeff α n (inv.aux a φ) = if n = 0 then a else
id                                         
typ                                        
560    - a * n.antidiagonal.support.sum (λ (x : (σ →₀ ℕ) × (σ →₀ ℕ)),
id                                                          
src                                                             
typ                                                         
561      if x.2 < n then coeff α x.1 φ * coeff α x.2 (inv.aux a φ) else 0) :=
id                                                         
typ                                                        
562  show inv.aux a φ n = _, by { rw inv.aux, refl }
id                
typ               
st                                                 └┘
563  
564  /-- A multivariate formal power series is invertible if the constant coefficient is invertible.-/
565  def inv_of_unit (φ : mv_power_series σ α) (u : units α) : mv_power_series σ α :=
id                                                                           
typ                                                                          
566  inv.aux (↑u⁻¹) φ
id                  
typ                 
567  
568  lemma coeff_inv_of_unit (n : σ →₀ ℕ) (φ : mv_power_series σ α) (u : units α) :
id                                                                         
src                                    
typ                                                                        
569    coeff α n (inv_of_unit φ u) = if n = 0 then ↑u⁻¹ else
id                                   
typ                                  
570    - ↑u⁻¹ * n.antidiagonal.support.sum (λ (x : (σ →₀ ℕ) × (σ →₀ ℕ)),
id                                                              
src                                                                
typ                                                             
571      if x.2 < n then coeff α x.1 φ * coeff α x.2 (inv_of_unit φ u) else 0) :=
id                                                            
typ                                                           
572  coeff_inv_aux n (↑u⁻¹) φ
573  
574  @[simp] lemma constant_coeff_inv_of_unit (φ : mv_power_series σ α) (u : units α) :
id                                                                               
typ                                                                              
doc    └──┘
575    constant_coeff σ α (inv_of_unit φ u) = ↑u⁻¹ :=
id                                   
typ                                  
576  by rw [← coeff_zero_eq_constant_coeff_apply, coeff_inv_of_unit, if_pos rfl]
st                                                                             
577  
578  lemma mul_inv_of_unit (φ : mv_power_series σ α) (u : units α) (h : constant_coeff σ α φ = u) :
id                                                                                    
typ                                                                                   
579    φ * inv_of_unit φ u = 1 :=
id                    
typ                   
580  ext $ λ n, if H : n = 0 then by { rw H, simp [coeff_mul, support_single_ne_zero, h], }
id           
typ          
st                                                                                        └┘
581  else
582  begin
583    have : ((0 : σ →₀ ℕ), n) ∈ n.antidiagonal.support,
id                  
typ                 
584    { rw [finsupp.mem_antidiagonal_support, zero_add] },
st                                                      └┘
585    rw [coeff_one, if_neg H, coeff_mul,
586      ← finset.insert_erase this, finset.sum_insert (finset.not_mem_erase _ _),
587      coeff_zero_eq_constant_coeff_apply, h, coeff_inv_of_unit, if_neg H,
588      neg_mul_eq_neg_mul_symm, mul_neg_eq_neg_mul_symm, units.mul_inv_cancel_left,
589      ← finset.insert_erase this, finset.sum_insert (finset.not_mem_erase _ _),
590      finset.insert_erase this, if_neg (not_lt_of_ge $ le_refl _), zero_add, add_comm,
591      ← sub_eq_add_neg, sub_eq_zero, finset.sum_congr rfl],
592    rintros ⟨i,j⟩ hij, rw [finset.mem_erase, finsupp.mem_antidiagonal_support] at hij,
593    cases hij with h₁ h₂,
594    subst n, rw if_pos,
id           
typ          
595    suffices : (0 : _) + j < i + j, {simpa},
id                              
typ                             
st                                           └┘
596    apply add_lt_add_right,
597    split,
598    { intro s, exact nat.zero_le _ },
st                                    └┘
599    { intro H, apply h₁,
600      suffices : i = 0, {simp [this]},
id                  
typ                 
st                                     └┘
601      ext1 s, exact nat.eq_zero_of_le_zero (H s) }
id                                               
typ                                              
st                                                  └┘
602  end
603  
604  end ring
605  
606  section comm_ring
607  variable [comm_ring α]
id             └──┘  └─┘
src            └──┘  └─┘
typ            └──┘  └─┘
608  
609  /-- Multivariate formal power series over a local ring form a local ring.-/
610  lemma is_local_ring (h : is_local_ring α) : is_local_ring (mv_power_series σ α) :=
id                                                                              
typ                                                                             
611  begin
612    split,
613    { have H : (0:α) ≠ 1 := ‹is_local_ring α›.1, contrapose! H,
id                                           
typ                                          
614      simpa using congr_arg (constant_coeff σ α) H },
id                                              
typ                                             
st                                                    └┘
615    { intro φ, rcases ‹is_local_ring α›.2 (constant_coeff σ α φ) with ⟨u,h⟩|⟨u,h⟩; [left, right];
id                                                                                  └──┘  └───┘
src                                                                                    └──┘  └───┘
typ                                                                                 └──┘  └───┘
doc                                                                                    └──┘  └───┘
616      { refine is_unit_of_mul_one _ _ (mul_inv_of_unit _ u _),
617        simpa using h } }
st                       └───
618  end
st   ──┘
619  
620  -- TODO(jmc): once adic topology lands, show that this is complete
621  
622  end comm_ring
623  
624  section nonzero_comm_ring
625  variables [nonzero_comm_ring α]
id              └┘  └──┘  └──┘  
src             └┘  └──┘  └──┘  
typ             └┘  └──┘  └──┘  
doc             └┘  └──┘  └──┘  
626  
627  instance : nonzero_comm_ring (mv_power_series σ α) :=
id                                                  
typ                                                 
628  { zero_ne_one := assume h, zero_ne_one $ show (0:α) = 1, from congr_arg (constant_coeff σ α) h,
id                                                                                           
typ                                                                                          
629    .. mv_power_series.comm_ring }
630  
631  lemma X_inj {s t : σ} : (X s : mv_power_series σ α) = X t ↔ s = t :=
id                                                             
src                                                            
typ                                                            
632  ⟨begin
633    intro h, replace h := congr_arg (coeff α (single s 1)) h, rw [coeff_X, if_pos rfl, coeff_X] at h,
id                                                     
typ                                                    
634    split_ifs at h with H,
635    { rw finsupp.single_eq_single_iff at H,
636      cases H, { exact H.1 }, { exfalso, exact one_ne_zero H.1 } },
st                            └┘                                  └──┘
637    { exfalso, exact one_ne_zero h }
st                                    └─
638  end, congr_arg X⟩
st   ──┘
639  
640  end nonzero_comm_ring
641  
642  section local_ring
643  variables {β : Type*} [local_ring α] [local_ring β] (f : α →+* β) [is_local_ring_hom f]
id                          └┘  └──┘         └──┘  └┘
src                         └┘  └──┘         └──┘  └┘
typ                         └┘  └──┘         └──┘  └┘
644  
645  instance : local_ring (mv_power_series σ α) :=
id                                           
typ                                          
646  local_of_is_local_ring $ is_local_ring ⟨zero_ne_one, local_ring.is_local⟩
647  
648  instance map.is_local_ring_hom :
649    is_local_ring_hom (map σ f : mv_power_series σ α → mv_power_series σ β) :=
id                                                                      
typ                                                                     
650  { map_one := (map σ f).map_one,
id                     
typ                    
651    map_mul := (map σ f).map_mul,
id                     
typ                    
652    map_add := (map σ f).map_add,
id                     
typ                    
653    map_nonunit :=
654    begin
655      rintros φ ⟨ψ, h⟩,
656      replace h := congr_arg (constant_coeff σ β) h,
id                                               
typ                                              
657      rw constant_coeff_map at h,
658      have : is_unit (constant_coeff σ β ↑ψ) := @is_unit_constant_coeff σ β _ (↑ψ) (is_unit_unit ψ),
id                                                                        
typ                                                                       
659      rw ← h at this,
660      rcases is_unit_of_map_unit f _ this with ⟨c, hc⟩,
661      exact is_unit_of_mul_one φ (inv_of_unit φ c) (mul_inv_of_unit φ c hc)
662    end }
st     └─┘
663  
664  end local_ring
665  
666  section discrete_field
667  variables [discrete_field α]
id              └┘  └──┘  └──┘
src             └┘  └──┘  └──┘
typ             └┘  └──┘  └──┘
668  
669  protected def inv (φ : mv_power_series σ α) : mv_power_series σ α :=
id                                                                
typ                                                               
670  inv.aux (constant_coeff σ α φ)⁻¹ φ
id                                 
typ                                
671  
672  instance : has_inv (mv_power_series σ α) := ⟨mv_power_series.inv⟩
id                                        
typ                                       
673  
674  lemma coeff_inv (n : σ →₀ ℕ) (φ : mv_power_series σ α) :
id                                                    
src                            
typ                                                   
675    coeff α n (φ⁻¹) = if n = 0 then (constant_coeff σ α φ)⁻¹ else
id                                                   
typ                                                  
676    - (constant_coeff σ α φ)⁻¹ * n.antidiagonal.support.sum (λ (x : (σ →₀ ℕ) × (σ →₀ ℕ)),
id                                                                               
src                                                                                    
typ                                                                              
677      if x.2 < n then coeff α x.1 φ * coeff α x.2 (φ⁻¹) else 0) :=
id                                                
typ                                               
678  coeff_inv_aux n _ φ
679  
680  @[simp] lemma constant_coeff_inv (φ : mv_power_series σ α) :
id                                                          
typ                                                         
doc    └──┘
681    constant_coeff σ α (φ⁻¹) = (constant_coeff σ α φ)⁻¹ :=
id                                               
typ                                              
682  by rw [← coeff_zero_eq_constant_coeff_apply, coeff_inv, if_pos rfl]
st                                                                     
683  
684  lemma inv_eq_zero {φ : mv_power_series σ α} :
id                                           
typ                                          
685    φ⁻¹ = 0 ↔ constant_coeff σ α φ = 0 :=
id                              
src            
typ                             
686  ⟨λ h, by simpa using congr_arg (constant_coeff σ α) h,
id                                                   
typ                                                  
687   λ h, ext $ λ n, by { rw coeff_inv, split_ifs;
id                 
typ                
688   simp only [h, mv_power_series.coeff_zero, zero_mul, inv_zero, neg_zero] }⟩
st                                                                            └┘
689  
690  @[simp] lemma inv_of_unit_eq (φ : mv_power_series σ α) (h : constant_coeff σ α φ ≠ 0) :
id                                                                              
typ                                                                             
doc    └──┘
691    inv_of_unit φ (units.mk0 _ h) = φ⁻¹ := rfl
id                                    
typ                                   
692  
693  @[simp] lemma inv_of_unit_eq' (φ : mv_power_series σ α) (u : units α) (h : constant_coeff σ α φ = u) :
id                                                                                            
typ                                                                                           
doc    └──┘
694    inv_of_unit φ u = φ⁻¹ :=
id                      
typ                     
695  begin
696    rw ← inv_of_unit_eq φ (h.symm ▸ u.ne_zero),
697    congr' 1, rw [units.ext_iff], exact h.symm,
698  end
st   └─┘
699  
700  @[simp] protected lemma mul_inv (φ : mv_power_series σ α) (h : constant_coeff σ α φ ≠ 0) :
id                                                                                 
typ                                                                                
doc    └──┘
701    φ * φ⁻¹ = 1 :=
id        
typ       
702  by rw [← inv_of_unit_eq φ h, mul_inv_of_unit φ (units.mk0 _ h) rfl]
703  
704  @[simp] protected lemma inv_mul (φ : mv_power_series σ α) (h : constant_coeff σ α φ ≠ 0) :
id                                                                                 
typ                                                                                
doc    └──┘
705    φ⁻¹ * φ = 1 :=
id          
typ         
706  by rw [mul_comm, φ.mul_inv h]
707  
708  end discrete_field
709  
710  end mv_power_series
711  
712  namespace mv_polynomial
713  open finsupp
714  variables {σ : Type*} {α : Type*} [comm_semiring α]
id                                        └┘  └┘  └┘
src                                       └┘  └┘  └┘
typ                                       └┘  └┘  └┘
715  
716  /-- The natural inclusion from multivariate polynomials into multivariate formal power series.-/
717  instance coe_to_mv_power_series : has_coe (mv_polynomial σ α) (mv_power_series σ α) :=
id                                                                                 
typ                                                                                
718  ⟨λ φ n, coeff n φ⟩
id                
typ               
719  
720  @[simp, elim_cast] lemma coeff_coe (φ : mv_polynomial σ α) (n : σ →₀ ℕ) :
id                                                                     
src                                                                       
typ                                                                    
doc    └──┘  └───────┘
721  mv_power_series.coeff α n ↑φ = coeff n φ := rfl
id                                      
typ                                     
722  
723  @[simp, elim_cast] lemma coe_monomial (n : σ →₀ ℕ) (a : α) :
id                                                         
src                                                  
typ                                                        
doc    └──┘  └───────┘
724    (monomial n a : mv_power_series σ α) = mv_power_series.monomial α n a :=
id                                                                   
typ                                                                  
725  mv_power_series.ext $ λ m,
id                           
typ                          
726  begin
727    rw [coeff_coe, coeff_monomial, mv_power_series.coeff_monomial],
728    split_ifs with h₁ h₂; refl <|> subst m; contradiction
id                           └──┘              └───────────┘
src                          └──┘              └───────────┘
typ                          └──┘              └───────────┘
doc                          └──┘              └───────────┘
729  end
st   └─┘
730  
731  @[simp, elim_cast] lemma coe_zero : ((0 : mv_polynomial σ α) : mv_power_series σ α) = 0 := rfl
id                                                                                 
typ                                                                                
doc    └──┘  └───────┘
732  
733  @[simp, elim_cast] lemma coe_one : ((1 : mv_polynomial σ α) : mv_power_series σ α) = 1 :=
id                                                                                
typ                                                                               
doc    └──┘  └───────┘
734  coe_monomial _ _
735  
736  @[simp, elim_cast] lemma coe_add (φ ψ : mv_polynomial σ α) :
id                                                          
typ                                                         
doc    └──┘  └───────┘
737    ((φ + ψ : mv_polynomial σ α) : mv_power_series σ α) = φ + ψ := rfl
id                                                        
typ                                                       
738  
739  @[simp, elim_cast] lemma coe_mul (φ ψ : mv_polynomial σ α) :
id                                                          
typ                                                         
doc    └──┘  └───────┘
740    ((φ * ψ : mv_polynomial σ α) : mv_power_series σ α) = φ * ψ :=
id                                                         
typ                                                        
741  mv_power_series.ext $ λ n,
id                           
typ                          
742  by simp only [coeff_coe, mv_power_series.coeff_mul, coeff_mul]
743  
744  @[simp, elim_cast] lemma coe_C (a : α) :
id                                       
typ                                      
doc    └──┘  └───────┘
745    ((C a : mv_polynomial σ α) : mv_power_series σ α) = mv_power_series.C σ α a :=
id                                                                        
typ                                                                       
746  coe_monomial _ _
747  
748  @[simp, elim_cast] lemma coe_X (s : σ) :
id                                       
typ                                      
doc    └──┘  └───────┘
749    ((X s : mv_polynomial σ α) : mv_power_series σ α) = mv_power_series.X s :=
id                                                                      
typ                                                                     
750  coe_monomial _ _
751  
752  namespace coe_to_mv_power_series
753  
754  instance : is_semiring_hom (coe : mv_polynomial σ α → mv_power_series σ α) :=
id                                                                        
typ                                                                       
755  { map_zero := coe_zero,
756    map_one := coe_one,
757    map_add := coe_add,
758    map_mul := coe_mul }
759  
760  end coe_to_mv_power_series
761  
762  end mv_polynomial
763  
764  /-- Formal power series over the coefficient ring `α`.-/
765  def power_series (α : Type*) := mv_power_series unit α
id                                                   └──┘ 
src                                                  └──┘
typ                                                  └──┘ 
doc                                                  └──┘
766  
767  namespace power_series
768  open finsupp (single)
769  variable {α : Type*}
id            
typ           
770  
771  instance [inhabited α]       : inhabited       (power_series α) := by delta power_series; apply_instance
id              └┘ └┘ └┘                            └┘  └┘  └┘                               └────────────┘
src             └┘ └┘ └┘                             └┘  └┘  └┘                                └────────────┘
typ             └┘ └┘ └┘                            └┘  └┘  └┘                               └────────────┘
doc                                                  └┘  └┘  └┘                                └────────────┘
772  instance [add_monoid α]      : add_monoid      (power_series α) := by delta power_series; apply_instance
id             └──┘  └──┘            └┘  └┘         └┘  └┘  └┘                               └────────────┘
src            └──┘  └──┘             └┘  └┘         └┘  └┘  └┘                                └────────────┘
typ            └──┘  └──┘            └┘  └┘         └┘  └┘  └┘                               └────────────┘
doc                                                  └┘  └┘  └┘                                └────────────┘
773  instance [add_group α]       : add_group       (power_series α) := by delta power_series; apply_instance
id             └──┘  └─┘             └┘  └┘          └┘  └┘  └┘                              └────────────┘
src            └──┘  └─┘              └┘  └┘          └┘  └┘  └┘                               └────────────┘
typ            └──┘  └─┘             └┘  └┘          └┘  └┘  └┘                              └────────────┘
doc                                                   └┘  └┘  └┘                               └────────────┘
774  instance [add_comm_monoid α] : add_comm_monoid (power_series α) := by delta power_series; apply_instance
id             └──┘  └──┘  └─┘       └┘  └┘  └┘      └┘  └┘                               └────────────┘
src            └──┘  └──┘  └─┘        └┘  └┘  └┘      └┘  └┘                                └────────────┘
typ            └──┘  └──┘  └─┘       └┘  └┘  └┘      └┘  └┘                               └────────────┘
doc                                                    └┘  └┘                                └────────────┘
775  instance [add_comm_group α]  : add_comm_group  (power_series α) := by delta power_series; apply_instance
id             └──┘  └──┘  └┘        └┘  └┘  └┘     └┘  └┘  └┘                               └────────────┘
src            └──┘  └──┘  └┘         └┘  └┘  └┘     └┘  └┘  └┘                                └────────────┘
typ            └──┘  └──┘  └┘        └┘  └┘  └┘     └┘  └┘  └┘                               └────────────┘
doc                                                  └┘  └┘  └┘                                └────────────┘
776  instance [semiring α]        : semiring        (power_series α) := by delta power_series; apply_instance
id             └──┘  └┘              └┘  └┘           └┘  └┘  └┘                             └────────────┘
src            └──┘  └┘               └┘  └┘           └┘  └┘  └┘                              └────────────┘
typ            └──┘  └┘              └┘  └┘           └┘  └┘  └┘                             └────────────┘
doc                                                    └┘  └┘  └┘                              └────────────┘
777  instance [comm_semiring α]   : comm_semiring   (power_series α) := by delta power_series; apply_instance
id             └──┘  └──┘           └┘  └┘  └┘      └┘  └┘  └┘                             └────────────┘
src            └──┘  └──┘            └┘  └┘  └┘      └┘  └┘  └┘                              └────────────┘
typ            └──┘  └──┘           └┘  └┘  └┘      └┘  └┘  └┘                             └────────────┘
doc                                                    └┘  └┘  └┘                              └────────────┘
778  instance [ring α]            : ring            (power_series α) := by delta power_series; apply_instance
id             └──┘                                └┘  └┘  └┘                              └────────────┘
src            └──┘                                 └┘  └┘  └┘                               └────────────┘
typ            └──┘                                └┘  └┘  └┘                              └────────────┘
doc                                                   └┘  └┘  └┘                               └────────────┘
779  instance [comm_ring α]       : comm_ring       (power_series α) := by delta power_series; apply_instance
id             └──┘  └─┘             └┘  └┘          └┘  └┘  └┘                              └────────────┘
src            └──┘  └─┘              └┘  └┘          └┘  └┘  └┘                               └────────────┘
typ            └──┘  └─┘             └┘  └┘          └┘  └┘  └┘                              └────────────┘
doc                                                   └┘  └┘  └┘                               └────────────┘
780  instance [nonzero_comm_ring α] : nonzero_comm_ring (power_series α) := by delta power_series; apply_instance
id             └──┘  └──┘  └──┘       └┘  └┘  └┘  └┘    └┘  └┘  └┘                               └────────────┘
src            └──┘  └──┘  └──┘        └┘  └┘  └┘  └┘    └┘  └┘  └┘                                └────────────┘
typ            └──┘  └──┘  └──┘       └┘  └┘  └┘  └┘    └┘  └┘  └┘                               └────────────┘
doc            └──┘  └──┘  └──┘        └┘  └┘  └┘  └┘    └┘  └┘  └┘                                └────────────┘
781  instance [semiring α]        : semimodule α    (power_series α) := by delta power_series; apply_instance
id             └──┘  └┘                            └─┘  └┘  └┘                              └────────────┘
src            └──┘  └┘                              └─┘  └┘  └┘                               └────────────┘
typ            └──┘  └┘                            └─┘  └┘  └┘                              └────────────┘
doc                                                  └─┘  └┘  └┘                               └────────────┘
782  instance [ring α]            : module α        (power_series α) := by delta power_series; apply_instance
id             └──┘                                 └┘  └┘  └┘                              └────────────┘
src            └──┘                                   └┘  └┘  └┘                               └────────────┘
typ            └──┘                                 └┘  └┘  └┘                              └────────────┘
doc                                                   └┘  └┘  └┘                               └────────────┘
783  instance [comm_ring α]       : algebra α       (power_series α) := by delta power_series; apply_instance
id             └──┘  └─┘                             └┘  └┘                               └────────────┘
src            └──┘  └─┘                               └┘  └┘                                └────────────┘
typ            └──┘  └─┘                             └┘  └┘                               └────────────┘
doc                                                    └┘  └┘                                └────────────┘
784  
785  section add_monoid
786  variables (α) [add_monoid α]
id                  └──┘  └──┘
src                 └──┘  └──┘
typ                 └──┘  └──┘
787  
788  /-- The `n`th coefficient of a formal power series.-/
789  def coeff (n : ℕ) : power_series α →+ α := mv_power_series.coeff α (single () n)
id                        └┘  └┘  └┘                                        └┘ 
src                       └┘  └┘  └┘                                           └┘
typ                       └┘  └┘  └┘                                        └┘ 
doc                        └┘  └┘  └┘
790  
791  /-- The `n`th monomial with coefficient `a` as formal power series.-/
792  def monomial (n : ℕ) : α →+ power_series α := mv_power_series.monomial α (single () n)
id                             └┘  └┘  └┘                                         └┘ 
src                             └┘  └┘  └┘                                           └┘
typ                            └┘  └┘  └┘                                         └┘ 
doc                              └┘  └┘  └┘
793  
794  variables {α}
795  
796  lemma coeff_def {s : unit →₀ ℕ} {n : ℕ} (h : s () = n) :
id                        └──┘                   └┘   
src                       └──┘                    └┘
typ                       └──┘                   └┘   
doc                       └──┘
797    coeff α n = mv_power_series.coeff α s :=
id                                      
typ                                     
798  by erw [coeff, ← h, ← finsupp.unique_single s]
id                                               
typ                                              
st                                                
799  
800  /-- Two formal power series are equal if all their coefficients are equal.-/
801  @[ext] lemma ext {φ ψ : power_series α} (h : ∀ n, coeff α n φ = coeff α n ψ) :
id                                                                      
typ                                                                     
doc    └─┘
802    φ = ψ :=
id        
typ       
803  mv_power_series.ext $ λ n,
id                           
typ                          
804  by { rw ← coeff_def, { apply h }, refl }
st                                  └┘      └┘
805  
806  /-- Two formal power series are equal if all their coefficients are equal.-/
807  lemma ext_iff {φ ψ : power_series α} : φ = ψ ↔ (∀ n, coeff α n φ = coeff α n ψ) :=
id                                                                      
src                                               
typ                                                                     
808  ⟨λ h n, congr_arg (coeff α n) h, ext⟩
id                            
typ                           
809  
810  /-- Constructor for formal power series.-/
811  def mk (f : ℕ → α) : power_series α := λ s, f (s ())
id                        └┘  └┘  └┘              └┘
src                        └┘  └┘  └┘                └┘
typ                       └┘  └┘  └┘              └┘
doc                         └┘  └┘  └┘
812  
813  @[simp] lemma coeff_mk (n : ℕ) (f : ℕ → α) : coeff α n (mk f) = f n :=
id                                                              
src                                     
typ                                                             
doc    └──┘
814  congr_arg f finsupp.single_eq_same
id             
typ            
815  
816  lemma coeff_monomial (m n : ℕ) (a : α) :
id                                       
typ                                      
817    coeff α m (monomial α n a) = if m = n then a else 0 :=
id                                         
typ                                        
818  calc coeff α m (monomial α n a) = _ : mv_power_series.coeff_monomial _ _ _
id                            
typ                           
819      ... = if m = n then a else 0 :
id                         
typ                        
820  by { simp only [finsupp.unique_single_eq_iff], split_ifs; refl }
id                                                             └──┘
src                                                            └──┘
typ                                                            └──┘
doc                                                            └──┘
st                                                                  └┘
821  
822  lemma monomial_eq_mk (n : ℕ) (a : α) :
id                                    
src                            
typ                                   
823    monomial α n a = mk (λ m, if m = n then a else 0) :=
id                                       
typ                                      
824  ext $ λ m, by { rw [coeff_monomial, coeff_mk] }
id           
typ          
st                                                └┘
825  
826  @[simp] lemma coeff_monomial' (n : ℕ) (a : α) :
id                                             
src                                     
typ                                            
doc    └──┘
827    coeff α n (monomial α n a) = a :=
id                             
typ                            
828  by convert if_pos rfl
829  
830  @[simp] lemma coeff_comp_monomial (n : ℕ) :
id                                          
src                                         
typ                                         
doc    └──┘
831    (coeff α n).comp (monomial α n) = add_monoid_hom.id α :=
id                                                     
typ                                                    
832  add_monoid_hom.ext $ coeff_monomial' n
id                                        
typ                                       
833  
834  end add_monoid
835  
836  section semiring
837  variable [semiring α]
id               └──┘
src              └──┘
typ              └──┘
838  
839  variable (α)
840  
841  /--The constant coefficient of a formal power series. -/
842  def constant_coeff : power_series α →+* α := mv_power_series.constant_coeff unit α
id                          └┘  └┘  └┘                                         └──┘ 
src                         └┘  └┘  └┘                                           └──┘
typ                         └┘  └┘  └┘                                         └──┘ 
doc                         └┘  └┘  └┘                                           └──┘
843  
844  /-- The constant formal power series.-/
845  def C : α →+* power_series α := mv_power_series.C unit α
id                └┘  └┘  └┘                         └──┘ 
src                └┘  └┘  └┘                          └──┘
typ               └┘  └┘  └┘                         └──┘ 
doc                └┘  └┘  └┘                          └──┘
846  
847  variable {α}
848  
849  /-- The variable of the formal power series ring.-/
850  def X : power_series α := mv_power_series.X ()
id             └┘  └┘  └┘                       └┘
src            └┘  └┘  └┘                        └┘
typ            └┘  └┘  └┘                       └┘
doc            └┘  └┘  └┘
851  
852  @[simp] lemma coeff_zero_eq_constant_coeff :
doc    └──┘
853    coeff α 0 = constant_coeff α :=
id                               
typ                              
854  begin
855    rw [constant_coeff, ← mv_power_series.coeff_zero_eq_constant_coeff, coeff_def], refl
856  end
st   └─┘
857  
858  @[simp] lemma coeff_zero_eq_constant_coeff_apply (φ : power_series α) :
id                                                           └┘  └┘  └┘ 
src                                                          └┘  └┘  └┘
typ                                                          └┘  └┘  └┘ 
doc    └──┘                                                  └┘  └┘  └┘
859    coeff α 0 φ = constant_coeff α φ :=
id                                 
typ                                
860  by rw [coeff_zero_eq_constant_coeff]; refl
id                                         └──┘
src                                        └──┘
typ                                        └──┘
doc                                        └──┘
861  
862  @[simp] lemma monomial_zero_eq_C : monomial α 0 = C α :=
id                                                      
typ                                                     
doc    └──┘
863  by rw [monomial, finsupp.single_zero, mv_power_series.monomial_zero_eq_C, C]
st                                                                              
864  
865  @[simp] lemma monomial_zero_eq_C_apply (a : α) : monomial α 0 a = C α a :=
id                                                                     
typ                                                                    
doc    └──┘
866  by rw [monomial_zero_eq_C]; refl
id                               └──┘
src                              └──┘
typ                              └──┘
doc                              └──┘
867  
868  lemma coeff_C (n : ℕ) (a : α) :
id                             
src                     
typ                            
869    coeff α n (C α a : power_series α) = if n = 0 then a else 0 :=
id                      └┘  └┘  └┘                  
src                         └┘  └┘  └┘
typ                     └┘  └┘  └┘                  
doc                         └┘  └┘  └┘
870  by rw [← monomial_zero_eq_C_apply, coeff_monomial]
871  
872  @[simp] lemma coeff_zero_C (a : α) : coeff α 0 (C α a) = a :=
id                                                        
typ                                                       
doc    └──┘
873  by rw [← monomial_zero_eq_C_apply, coeff_monomial' 0 a]
874  
875  lemma X_eq : (X : power_series α) = monomial α 1 1 := rfl
id                     └┘  └┘  └┘                
src                    └┘  └┘  └┘
typ                    └┘  └┘  └┘                
doc                    └┘  └┘  └┘
876  
877  lemma coeff_X (n : ℕ) :
id                      
src                     
typ                     
878    coeff α n (X : power_series α) = if n = 1 then 1 else 0 :=
id                    └┘  └┘          
src                     └┘  └┘  
typ                   └┘  └┘          
doc                     └┘  └┘  
879  by rw [X_eq, coeff_monomial]
880  
881  @[simp] lemma coeff_zero_X : coeff α 0 (X : power_series α) = 0 :=
id                                                └┘  └┘   
src                                                └┘  └┘  
typ                                               └┘  └┘   
doc    └──┘                                        └┘  └┘  
882  by rw [coeff, finsupp.single_zero, X, mv_power_series.coeff_zero_X]
st                                                                     
883  
884  @[simp] lemma coeff_one_X : coeff α 1 (X : power_series α) = 1 :=
id                                               └┘  └┘   
src                                               └┘  └┘  
typ                                              └┘  └┘   
doc    └──┘                                       └┘  └┘  
885  by rw [coeff_X, if_pos rfl]
886  
887  lemma X_pow_eq (n : ℕ) : (X : power_series α)^n = monomial α n 1 :=
id                                └┘ └┘  └┘                  
src                               └┘ └┘  └┘  
typ                               └┘ └┘  └┘                  
doc                                └┘ └┘  └┘  
888  mv_power_series.X_pow_eq _ n
id                              
typ                             
889  
890  lemma coeff_X_pow (m n : ℕ) :
id                            
src                           
typ                           
891    coeff α m ((X : power_series α)^n) = if m = n then 1 else 0 :=
id                   └┘  └┘  └┘               
src                    └┘  └┘  └┘
typ                  └┘  └┘  └┘               
doc                    └┘  └┘  └┘
892  by rw [X_pow_eq, coeff_monomial]
st                                  
893  
894  @[simp] lemma coeff_X_pow_self (n : ℕ) :
id                                       
src                                      
typ                                      
doc    └──┘
895    coeff α n ((X : power_series α)^n) = 1 :=
id                   └┘  └┘  └┘     
src                    └┘  └┘  └┘
typ                  └┘  └┘  └┘     
doc                    └┘  └┘  └┘
896  by rw [coeff_X_pow, if_pos rfl]
897  
898  @[simp] lemma coeff_one (n : ℕ) :
id                                
src                               
typ                               
doc    └──┘
899    coeff α n (1 : power_series α) = if n = 0 then 1 else 0 :=
id                    └┘  └┘          
src                     └┘  └┘  
typ                   └┘  └┘          
doc                     └┘  └┘  
900  calc coeff α n (1 : power_series α) = _ : mv_power_series.coeff_one _
id                       └┘  └┘  └┘
src                        └┘  └┘  └┘
typ                      └┘  └┘  └┘
doc                        └┘  └┘  └┘
901      ... = if n = 0 then 1 else 0 :
id                
typ               
902  by { simp only [finsupp.single_eq_zero], split_ifs; refl }
id                                                       └──┘
src                                                      └──┘
typ                                                      └──┘
doc                                                      └──┘
st                                                            └┘
903  
904  @[simp] lemma coeff_zero_one : coeff α 0 (1 : power_series α) = 1 :=
id                                                  └┘  └┘   
src                                                  └┘  └┘  
typ                                                 └┘  └┘   
doc    └──┘                                          └┘  └┘  
905  coeff_zero_C 1
906  
907  lemma coeff_mul (n : ℕ) (φ ψ : power_series α) :
id                                              
src                       
typ                                             
908    coeff α n (φ * ψ) = (finset.nat.antidiagonal n).sum (λ p, coeff α p.1 φ * coeff α p.2 ψ) :=
id                                                                               
typ                                                                              
909  begin
910    symmetry,
911    apply finset.sum_bij (λ (p : ℕ × ℕ) h, (single () p.1, single () p.2)),
912    { rintros ⟨i,j⟩ hij, rw finset.nat.mem_antidiagonal at hij,
913      rw [finsupp.mem_antidiagonal_support, ← finsupp.single_add, hij], },
st                                                                        └┘
914    { rintros ⟨i,j⟩ hij, refl },
st                               └┘
915    { rintros ⟨i,j⟩ ⟨k,l⟩ hij hkl,
916      simpa only [prod.mk.inj_iff, finsupp.unique_single_eq_iff] using id },
st                                                                           └┘
917    { rintros ⟨f,g⟩ hfg,
918      refine ⟨(f (), g ()), _, _⟩,
id                     
typ                    
919      { rw finsupp.mem_antidiagonal_support at hfg,
920        rw [finset.nat.mem_antidiagonal, ← finsupp.add_apply, hfg, finsupp.single_eq_same] },
st                                                                                           └┘
921      { rw prod.mk.inj_iff, dsimp,
922        exact ⟨finsupp.unique_single f, finsupp.unique_single g⟩ } }
id                                                              
typ                                                             
st                                                                  └───
923  end
st   ──┘
924  
925  @[simp] lemma coeff_mul_C (n : ℕ) (φ : power_series α) (a : α) :
id                                           └┘  └┘  └┘        
src                                          └┘  └┘  └┘
typ                                          └┘  └┘  └┘        
doc    └──┘                                   └┘  └┘  └┘
926    coeff α n (φ * (C α a)) = (coeff α n φ) * a :=
id                                       
typ                                      
927  mv_power_series.coeff_mul_C _ φ a
id                                  
typ                                 
928  
929  @[simp] lemma coeff_succ_mul_X (n : ℕ) (φ : power_series α) :
id                                                └┘  └┘  └┘ 
src                                               └┘  └┘  └┘
typ                                               └┘  └┘  └┘ 
doc    └──┘                                        └┘  └┘  └┘
930    coeff α (n+1) (φ * X) = coeff α n φ :=
id                                  
typ                                 
931  begin
932    rw [coeff_mul _ φ, finset.sum_eq_single (n,1)],
933    { rw [coeff_X, if_pos rfl, mul_one] },
st                                        └┘
934    { rintro ⟨i,j⟩ hij hne,
935      by_cases hj : j = 1,
id                     
typ                    
936      { subst hj, simp at *, contradiction },
st                                            └┘
937      { simp [coeff_X, hj] } },
st                            └──┘
938    { intro h, exfalso, apply h, simp },
st                                       └┘
939  end
st   └─┘
940  
941  @[simp] lemma coeff_zero_mul_X (φ : power_series α) :
id                                       └┘  └┘  └┘   
src                                      └┘  └┘  └┘
typ                                      └┘  └┘  └┘   
doc    └──┘                              └┘  └┘  └┘
942    coeff α 0 (φ * X) = 0 :=
id               
typ              
943  begin
944    rw [coeff_mul _ φ, finset.sum_eq_zero],
945    rintro ⟨i,j⟩ hij,
946    obtain ⟨rfl, rfl⟩ : i = 0 ∧ j = 0, { simpa using hij },
id                               
src                              
typ                              
st                                                          └┘
947    simp,
948  end
st   └─┘
949  
950  @[simp] lemma constant_coeff_C (a : α) : constant_coeff α (C α a) = a := rfl
id                                                                   
typ                                                                  
doc    └──┘
951  @[simp] lemma constant_coeff_comp_C :
doc    └──┘
952    (constant_coeff α).comp (C α) = ring_hom.id α := rfl
id                                               
typ                                              
953  
954  @[simp] lemma constant_coeff_zero : constant_coeff α 0 = 0 := rfl
id                                                      
typ                                                     
doc    └──┘
955  @[simp] lemma constant_coeff_one : constant_coeff α 1 = 1 := rfl
id                                                     
typ                                                    
doc    └──┘
956  @[simp] lemma constant_coeff_X : constant_coeff α X = 0 := mv_power_series.coeff_zero_X _
id                                                   
typ                                                  
doc    └──┘
957  
958  /-- If a formal power series is invertible, then so is its constant coefficient.-/
959  lemma is_unit_constant_coeff (φ : power_series α) (h : is_unit φ) :
id                                       └┘  └┘  └┘                
src                                      └┘  └┘  └┘
typ                                      └┘  └┘  └┘                
doc                                      └┘  └┘  └┘
960    is_unit (constant_coeff α φ) :=
id                              
typ                             
961  mv_power_series.is_unit_constant_coeff φ h
id                                          
typ                                         
962  
963  section map
964  variables {β : Type*} {γ : Type*} [semiring β] [semiring γ]
id                                        └┘       └─┘  └─┘
src                                       └┘       └─┘  └─┘
typ                                       └┘       └─┘  └─┘
965  variables (f : α →+* β) (g : β →+* γ)
966  
967  /-- The map between formal power series induced by a map on the coefficients.-/
968  def map : power_series α →+* power_series β :=
id               └┘  └┘  └┘      └┘  └┘  └┘   
src              └┘  └┘  └┘       └┘  └┘  └┘
typ              └┘  └┘  └┘      └┘  └┘  └┘   
doc              └┘  └┘  └┘       └┘  └┘  └┘
969  mv_power_series.map _ f
970  
971  @[simp] lemma map_id : (map (ring_hom.id α) :
id                                            
typ                                           
doc    └──┘
972    power_series α → power_series α) = id := rfl
id                      └┘  └┘  └┘  
src                      └┘  └┘  └┘
typ                     └┘  └┘  └┘  
doc                      └┘  └┘  └┘
973  
974  lemma map_comp : map (g.comp f) = (map g).comp (map f) := rfl
975  
976  @[simp] lemma coeff_map (n : ℕ) (φ : power_series α) :
id                                        └─┘  └┘  └┘ 
src                                       └─┘  └┘  └┘
typ                                       └─┘  └┘  └┘ 
doc    └──┘                                └─┘  └┘  └┘
977    coeff β n (map f φ) = f (coeff α n φ) := rfl
id                                  
typ                                 
978  
979  end map
980  
981  end semiring
982  
983  section comm_semiring
984  variables [comm_semiring α]
id                └──┘  └──┘
src               └──┘  └──┘
typ               └──┘  └──┘
985  
986  lemma X_pow_dvd_iff {n : ℕ} {φ : power_series α} :
id                                     └┘  └┘  └┘ 
src                                    └┘  └┘  └┘
typ                                    └┘  └┘  └┘ 
doc                                     └┘  └┘  └┘
987    (X : power_series α)^n ∣ φ ↔ ∀ m, m < n → coeff α m φ = 0 :=
id            └┘  └┘                            
src           └┘  └┘            
typ           └┘  └┘                            
doc           └┘  └┘  
988  begin
989    convert @mv_power_series.X_pow_dvd_iff unit α _ () n φ, apply propext,
id                                            └──┘    └┘  
src                                           └──┘     └┘
typ                                           └──┘    └┘  
doc                                           └──┘
990    classical, split; intros h m hm,
991    { rw finsupp.unique_single m, convert h _ hm },
id                                
typ                               
st                                                  └┘
992    { apply h, simpa only [finsupp.single_eq_same] using hm }
id                                                          └┘
typ                                                         └┘
st                                                             └─
993  end
st   ──┘
994  
995  lemma X_dvd_iff {φ : power_series α} :
id                        └┘  └┘  └┘   
src                       └┘  └┘  └┘
typ                       └┘  └┘  └┘   
doc                       └┘  └┘  └┘
996    (X : power_series α) ∣ φ ↔ constant_coeff α φ = 0 :=
id          └┘  └┘  └┘                          
src         └┘  └┘  └┘
typ         └┘  └┘  └┘                          
doc         └┘  └┘  └┘
997  begin
998    rw [← pow_one (X : power_series α), X_pow_dvd_iff, ← coeff_zero_eq_constant_coeff_apply],
999    split; intro h,
1000    { exact h 0 zero_lt_one },
st                             └┘
1001    { intros m hm, rwa nat.eq_zero_of_le_zero (nat.le_of_succ_le_succ hm) }
st                                                                           └─
1002  end
st   ──┘
1003  
1004  section trunc
1005  
1006  /-- The `n`th truncation of a formal power series to a polynomial -/
1007  def trunc (n : ℕ) (φ : power_series α) : polynomial α :=
id                           └┘  └┘  └┘                
src                          └┘  └┘  └┘
typ                          └┘  └┘  └┘                
doc                           └┘  └┘  └┘
1008  { support := ((finset.nat.antidiagonal n).image prod.fst).filter (λ m, coeff α m φ ≠ 0),
id                                                                                
typ                                                                               
1009    to_fun := λ m, if m ≤ n then coeff α m φ else 0,
id                                       
typ                                      
1010    mem_support_to_fun := λ m,
id                             
typ                            
1011    begin
1012      suffices : m ∈ ((finset.nat.antidiagonal n).image prod.fst) ↔ m ≤ n,
id                                                                        
typ                                                                       
1013      { rw [finset.mem_filter, this], split,
1014        { intro h, rw [if_pos h.1], exact h.2 },
st                                               └┘
1015        { intro h, split_ifs at h with H H,
1016          { exact ⟨H, h⟩ },
id                    
typ                   
st                          └┘
1017          { exfalso, exact h rfl } } },
st                                  └────┘
1018      rw finset.mem_image, split,
1019      { rintros ⟨⟨i,j⟩, h, rfl⟩,
1020        rw finset.nat.mem_antidiagonal at h,
1021        rw ← h, exact nat.le_add_right _ _ },
st                                            └┘
1022      { intro h, refine ⟨(m, n-m), _, rfl⟩,
id                               
typ                              
1023        rw finset.nat.mem_antidiagonal, exact nat.add_sub_of_le h }
id                                                                 
typ                                                                
st                                                                   └┘
1024    end }
st     └─┘
1025  
1026  lemma coeff_trunc (m) (n) (φ : power_series α) :
id                                  └┘  └┘  └┘   
src                                 └┘  └┘  └┘
typ                                 └┘  └┘  └┘   
doc                                 └┘  └┘  └┘
1027    polynomial.coeff (trunc n φ) m = if m ≤ n then coeff α m φ else 0 := rfl
id                                                       
typ                                                      
1028  
1029  @[simp] lemma trunc_zero (n) : trunc n (0 : power_series α) = 0 :=
id                                              └┘  └┘  └┘   
src                                              └┘  └┘  └┘
typ                                             └┘  └┘  └┘   
doc    └──┘                                      └┘  └┘  └┘
1030  polynomial.ext $ λ m,
id                      
typ                     
1031  begin
1032    rw [coeff_trunc, add_monoid_hom.map_zero, polynomial.coeff_zero],
1033    split_ifs; refl
id                └──┘
src               └──┘
typ               └──┘
doc               └──┘
1034  end
st   └─┘
1035  
1036  @[simp] lemma trunc_one (n) : trunc n (1 : power_series α) = 1 :=
id                                             └┘  └┘  └┘   
src                                             └┘  └┘  └┘
typ                                            └┘  └┘  └┘   
doc    └──┘                                     └┘  └┘  └┘
1037  polynomial.ext $ λ m,
id                      
typ                     
1038  begin
1039    rw [coeff_trunc, coeff_one],
1040    split_ifs with H H' H'; rw [polynomial.coeff_one],
1041    { subst m, rw [if_pos rfl] },
id             
typ            
st                               └┘
1042    { symmetry, exact if_neg (ne.elim (ne.symm H')) },
st                                                     └┘
1043    { symmetry, refine if_neg _,
1044      intro H', apply H, subst m, exact nat.zero_le _ }
id                                
typ                               
st                                                       └─
1045  end
st   ──┘
1046  
1047  @[simp] lemma trunc_C (n) (a : α) : trunc n (C α a) = polynomial.C a :=
id                                                                  
typ                                                                 
doc    └──┘
1048  polynomial.ext $ λ m,
id                      
typ                     
1049  
1050  begin
1051    rw [coeff_trunc, coeff_C, polynomial.coeff_C],
1052    split_ifs with H; refl <|> try {simp * at *}
id                       └──┘     └─┘
src                      └──┘     └─┘
typ                      └──┘     └─┘
doc                      └──┘     └─┘
st                                                └─
1053  end
st   ──┘
1054  
1055  @[simp] lemma trunc_add (n) (φ ψ : power_series α) :
id                                                   
typ                                                  
doc    └──┘
1056    trunc n (φ + ψ) = trunc n φ + trunc n ψ :=
id                                     
typ                                    
1057  polynomial.ext $ λ m,
id                      
typ                     
1058  begin
1059    simp only [coeff_trunc, add_monoid_hom.map_add, polynomial.coeff_add],
1060    split_ifs with H, {refl}, {rw [zero_add]}
st                            └┘              └──
1061  end
st   ──┘
1062  
1063  end trunc
1064  
1065  end comm_semiring
1066  
1067  section ring
1068  variables [ring α]
id              └┘
src             └┘
typ             └┘
1069  
1070  protected def inv.aux : α → power_series α → power_series α :=
id                                              └─┘  └┘  └┘  
src                                               └─┘  └┘  └┘
typ                                             └─┘  └┘  └┘  
doc                                               └─┘  └┘  └┘
1071  mv_power_series.inv.aux
1072  
1073  lemma coeff_inv_aux (n : ℕ) (a : α) (φ : power_series α) :
id                                            └┘  └┘  └┘ 
src                                            └┘  └┘  └┘
typ                                           └┘  └┘  └┘ 
doc                                             └┘  └┘  └┘
1074    coeff α n (inv.aux a φ) = if n = 0 then a else
id                                         
typ                                        
1075    - a * (finset.nat.antidiagonal n).sum (λ (x : ℕ × ℕ),
id                                                    
src                                                     
typ                                                   
1076      if x.2 < n then coeff α x.1 φ * coeff α x.2 (inv.aux a φ) else 0) :=
id                                                        
typ                                                       
1077  begin
1078    rw [coeff, inv.aux, mv_power_series.coeff_inv_aux],
1079    simp only [finsupp.single_eq_zero],
1080    split_ifs, {refl},
st                     └┘
1081    congr' 1,
1082    symmetry,
1083    apply finset.sum_bij (λ (p : ℕ × ℕ) h, (single () p.1, single () p.2)),
id                                                                   └┘
src                                                                  └┘
typ                                                                  └┘
1084    { rintros ⟨i,j⟩ hij, rw finset.nat.mem_antidiagonal at hij,
1085      rw [finsupp.mem_antidiagonal_support, ← finsupp.single_add, hij], },
st                                                                        └┘
1086    { rintros ⟨i,j⟩ hij,
1087      by_cases H : j < n,
id                       
typ                      
1088      { rw [if_pos H, if_pos], {refl},
id                    
typ                   
st                                     └┘
1089        split,
1090        { rintro ⟨⟩, simpa [finsupp.single_eq_same] using le_of_lt H },
id                                                                    
typ                                                                   
st                                                                      └┘
1091        { intro hh, rw lt_iff_not_ge at H, apply H,
1092          simpa [finsupp.single_eq_same] using hh () } },
id                                                   └┘
src                                                  └┘
typ                                                  └┘
st                                                      └──┘
1093      { rw [if_neg H, if_neg], rintro ⟨h₁, h₂⟩, apply h₂, rintro ⟨⟩,
id                    
typ                   
1094       simpa [finsupp.single_eq_same] using not_lt.1 H } },
st                                                        └──┘
1095    { rintros ⟨i,j⟩ ⟨k,l⟩ hij hkl,
1096      simpa only [prod.mk.inj_iff, finsupp.unique_single_eq_iff] using id },
st                                                                           └┘
1097    { rintros ⟨f,g⟩ hfg,
1098      refine ⟨(f (), g ()), _, _⟩,
id                     
typ                    
1099      { rw finsupp.mem_antidiagonal_support at hfg,
1100        rw [finset.nat.mem_antidiagonal, ← finsupp.add_apply, hfg, finsupp.single_eq_same] },
st                                                                                           └┘
1101      { rw prod.mk.inj_iff, dsimp,
1102        exact ⟨finsupp.unique_single f, finsupp.unique_single g⟩ } }
id                                                              
typ                                                             
st                                                                  └───
1103  end
st   ──┘
1104  
1105  /-- A formal power series is invertible if the constant coefficient is invertible.-/
1106  def inv_of_unit (φ : power_series α) (u : units α) : power_series α :=
id                          └┘  └┘  └┘                  └┘  └┘  └┘   
src                         └┘  └┘  └┘                    └┘  └┘  └┘
typ                         └┘  └┘  └┘                  └┘  └┘  └┘   
doc                         └┘  └┘  └┘                    └┘  └┘  └┘
1107  mv_power_series.inv_of_unit φ u
id                               
typ                              
1108  
1109  lemma coeff_inv_of_unit (n : ℕ) (φ : power_series α) (u : units α) :
id                                         └┘  └┘  └┘              
src                                        └┘  └┘  └┘
typ                                        └┘  └┘  └┘              
doc                                         └┘  └┘  └┘
1110    coeff α n (inv_of_unit φ u) = if n = 0 then ↑u⁻¹ else
id                                   
typ                                  
1111    - ↑u⁻¹ * (finset.nat.antidiagonal n).sum (λ (x : ℕ × ℕ),
id                                                        
src                                                        
typ                                                       
1112      if x.2 < n then coeff α x.1 φ * coeff α x.2 (inv_of_unit φ u) else 0) :=
id                                                          
typ                                                         
1113  coeff_inv_aux n ↑u⁻¹ φ
id                       
typ                      
1114  
1115  @[simp] lemma constant_coeff_inv_of_unit (φ : power_series α) (u : units α) :
id                                                 └┘  └┘  └┘                
src                                                └┘  └┘  └┘
typ                                                └┘  └┘  └┘                
doc    └──┘                                        └┘  └┘  └┘
1116    constant_coeff α (inv_of_unit φ u) = ↑u⁻¹ :=
id                                  
typ                                 
1117  by rw [← coeff_zero_eq_constant_coeff_apply, coeff_inv_of_unit, if_pos rfl]
st                                                                             
1118  
1119  lemma mul_inv_of_unit (φ : power_series α) (u : units α) (h : constant_coeff α φ = u) :
id                              └┘  └┘  └┘                                       
src                             └┘  └┘  └┘
typ                             └┘  └┘  └┘                                       
doc                             └┘  └┘  └┘
1120    φ * inv_of_unit φ u = 1 :=
id                    
typ                   
1121  mv_power_series.mul_inv_of_unit φ u $ h
id                                   
typ                                  
1122  
1123  end ring
1124  
1125  section integral_domain
1126  variable [integral_domain α]
id             └┘ └┘ └┘ └┘ └┘
src            └┘ └┘ └┘ └┘ └┘
typ            └┘ └┘ └┘ └┘ └┘
1127  
1128  lemma eq_zero_or_eq_zero_of_mul_eq_zero (φ ψ : power_series α) (h : φ * ψ = 0) :
id                                                                         
typ                                                                        
1129    φ = 0 ∨ ψ = 0 :=
id           
src          
typ          
1130  begin
1131      rw classical.or_iff_not_imp_left, intro H,
1132      have ex : ∃ m, coeff α m φ ≠ 0, { contrapose! H, exact ext H },
id                              
typ                             
st                                                                    └┘
1133      let P : ℕ → Prop := λ k, coeff α k φ ≠ 0,
id                                        
typ                                       
1134      let m := nat.find ex,
1135      have hm₁ : coeff α m φ ≠ 0 := nat.find_spec ex,
id                          
typ                         
1136      have hm₂ : ∀ k < m, ¬coeff α k φ ≠ 0 := λ k, nat.find_min ex,
id                                              
typ                                             
1137      ext n, rw (coeff α n).map_zero, apply nat.strong_induction_on n,
id                                                                   
typ                                                                  
1138      clear n, intros n ih,
1139      replace h := congr_arg (coeff α (m + n)) h,
id                                          
typ                                         
1140      rw [add_monoid_hom.map_zero, coeff_mul, finset.sum_eq_single (m,n)] at h,
id                                                                      
typ                                                                     
1141      { replace h := eq_zero_or_eq_zero_of_mul_eq_zero h,
1142        rw or_iff_not_imp_left at h, exact h hm₁ },
st                                                  └┘
1143      { rintro ⟨i,j⟩ hij hne,
1144        by_cases hj : j < n, { rw [ih j hj, mul_zero] },
id                                      └┘
typ                                     └┘
st                                                      └┘
1145        by_cases hi : i < m,
id                          
typ                         
1146        { specialize hm₂ _ hi, push_neg at hm₂, rw [hm₂, zero_mul] },
id                            └┘
typ                           └┘
st                                                                   └┘
1147        rw finset.nat.mem_antidiagonal at hij,
1148        push_neg at hi hj,
1149        suffices : m < i,
id                       
typ                      
1150        { have : m + n < i + j := add_lt_add_of_lt_of_le this hj,
id                                                      └──┘ └┘
typ                                                     └──┘ └┘
1151          exfalso, exact ne_of_lt this hij.symm },
st                                                 └┘
1152        contrapose! hne, have : i = m := le_antisymm hne hi, subst i, clear hi hne,
id                                                    └─┘ └┘        
typ                                                   └─┘ └┘        
1153        simpa [ne.def, prod.mk.inj_iff] using (add_left_inj m).mp hij },
id                                                             
typ                                                            
st                                                                       └┘
1154      { contrapose!, intro h, rw finset.nat.mem_antidiagonal }
st                                                              └─
1155  end
st   ──┘
1156  
1157  instance : integral_domain (power_series α) :=
id              └┘  └┘  └┘  └┘    └┘  └┘  └┘  
src             └┘  └┘  └┘  └┘    └┘  └┘  └┘
typ             └┘  └┘  └┘  └┘    └┘  └┘  └┘  
doc                               └┘  └┘  └┘
1158  { eq_zero_or_eq_zero_of_mul_eq_zero := eq_zero_or_eq_zero_of_mul_eq_zero,
1159    .. power_series.nonzero_comm_ring }
1160  
1161  /-- The ideal spanned by the variable in the power series ring
1162   over an integral domain is a prime ideal.-/
1163  lemma span_X_is_prime : (ideal.span ({X} : set (power_series α))).is_prime :=
id                                              └┘    └┘  └┘  └┘  
src                                             └┘    └┘  └┘  └┘
typ                                             └┘    └┘  └┘  └┘  
doc                                                   └┘  └┘  └┘
1164  begin
1165    suffices : ideal.span ({X} : set (power_series α)) = is_ring_hom.ker (constant_coeff α),
id                                  └─┘  └──────────┘                                       
src                                 └─┘  └──────────┘
typ                                 └─┘  └──────────┘                                       
doc                                      └──────────┘
1166    { rw this, exact is_ring_hom.ker_is_prime _ },
st                                                 └┘
1167    apply ideal.ext, intro φ,
1168    rw [is_ring_hom.mem_ker, ideal.mem_span_singleton, X_dvd_iff]
st                                                                 
1169  end
st   └─┘
1170  
1171  /-- The variable of the power series ring over an integral domain is prime.-/
1172  lemma X_prime : prime (X : power_series α) :=
id                              └┘  └┘  └┘   
src                             └┘  └┘  └┘
typ                             └┘  └┘  └┘   
doc                             └┘  └┘  └┘
1173  begin
1174    rw ← ideal.span_singleton_prime,
1175    { exact span_X_is_prime },
st                             └┘
1176    { intro h, simpa using congr_arg (coeff α 1) h }
id                                             
typ                                            
st                                                    └─
1177  end
st   ──┘
1178  
1179  end integral_domain
1180  
1181  section local_ring
1182  variables [comm_ring α]
id              └┘  └──┘
src             └┘  └──┘
typ             └┘  └──┘
1183  
1184  lemma is_local_ring (h : is_local_ring α) :
id                                          
typ                                         
1185    is_local_ring (power_series α) :=
id                    └┘  └┘  └┘   
src                   └┘  └┘  └┘
typ                   └┘  └┘  └┘   
doc                   └┘  └┘  └┘
1186  mv_power_series.is_local_ring h
id                                 
typ                                
1187  
1188  end local_ring
1189  
1190  section local_ring
1191  variables {β : Type*} [local_ring α] [local_ring β] (f : α →+* β) [is_local_ring_hom f]
id                           └──┘  └─┘     └─┘  └──┘
src                          └──┘  └─┘     └─┘  └──┘
typ                          └──┘  └─┘     └─┘  └──┘
1192  
1193  instance : local_ring (power_series α) :=
id              └┘  └┘  └┘    └┘  └┘  └┘ 
src             └┘  └┘  └┘    └┘  └┘  └┘
typ             └┘  └┘  └┘    └┘  └┘  └┘ 
doc                           └┘  └┘  └┘
1194  mv_power_series.local_ring
1195  
1196  instance map.is_local_ring_hom :
1197    is_local_ring_hom (map f) :=
1198  mv_power_series.map.is_local_ring_hom f
1199  
1200  end local_ring
1201  
1202  section discrete_field
1203  variables [discrete_field α]
id              └┘  └──┘  └──┘
src             └┘  └──┘  └──┘
typ             └┘  └──┘  └──┘
1204  
1205  protected def inv : power_series α → power_series α :=
id                                       └┘  └┘  └┘   
src                                       └┘  └┘  └┘
typ                                      └┘  └┘  └┘   
doc                                       └┘  └┘  └┘
1206  mv_power_series.inv
1207  
1208  instance : has_inv (power_series α) := ⟨power_series.inv⟩
id                └┘      └┘  └┘   
src               └┘      └┘  └┘  
typ               └┘      └┘  └┘   
doc                        └┘  └┘  
1209  
1210  lemma inv_eq_inv_aux (φ : power_series α) :
id                               └┘  └┘  └┘ 
src                              └┘  └┘  └┘
typ                              └┘  └┘  └┘ 
doc                              └┘  └┘  └┘
1211    φ⁻¹ = inv.aux (constant_coeff α φ)⁻¹ φ := rfl
id                                        
typ                                       
1212  
1213  lemma coeff_inv (n) (φ : power_series α) :
id                              └┘  └┘  └┘ 
src                             └┘  └┘  └┘
typ                             └┘  └┘  └┘ 
doc                             └┘  └┘  └┘
1214    coeff α n (φ⁻¹) = if n = 0 then (constant_coeff α φ)⁻¹ else
id                                                  
typ                                                 
1215    - (constant_coeff α φ)⁻¹ * (finset.nat.antidiagonal n).sum (λ (x : ℕ × ℕ),
id                                                                        
src                                                                          
typ                                                                       
1216      if x.2 < n then coeff α x.1 φ * coeff α x.2 (φ⁻¹) else 0) :=
id                                              
typ                                             
1217  by rw [inv_eq_inv_aux, coeff_inv_aux n (constant_coeff α φ)⁻¹ φ]
id                                                               
typ                                                              
st                                                                  
1218  
1219  @[simp] lemma constant_coeff_inv (φ : power_series α) :
id                                         └┘  └┘  └┘   
src                                        └┘  └┘  └┘
typ                                        └┘  └┘  └┘   
doc    └──┘                                └┘  └┘  └┘
1220    constant_coeff α (φ⁻¹) = (constant_coeff α φ)⁻¹ :=
id                                             
typ                                            
1221  mv_power_series.constant_coeff_inv φ
id                                      
typ                                     
1222  
1223  lemma inv_eq_zero {φ : power_series α} :
id                            └┘  └┘  └┘ 
src                           └┘  └┘  └┘
typ                           └┘  └┘  └┘ 
doc                           └┘  └┘  └┘
1224    φ⁻¹ = 0 ↔ constant_coeff α φ = 0 :=
id                              
src            
typ                             
1225  mv_power_series.inv_eq_zero
1226  
1227  @[simp] lemma inv_of_unit_eq (φ : power_series α) (h : constant_coeff α φ ≠ 0) :
id                                       └┘  └┘  └┘                        
src                                      └┘  └┘  └┘
typ                                      └┘  └┘  └┘                        
doc    └──┘                              └┘  └┘  └┘
1228    inv_of_unit φ (units.mk0 _ h) = φ⁻¹ :=
id                                    
typ                                   
1229  mv_power_series.inv_of_unit_eq _ _
1230  
1231  @[simp] lemma inv_of_unit_eq' (φ : power_series α) (u : units α) (h : constant_coeff α φ = u) :
id                                       └┘  └┘  └┘                                      
src                                      └┘  └┘  └┘
typ                                      └┘  └┘  └┘                                      
doc    └──┘                              └┘  └┘  └┘
1232    inv_of_unit φ u = φ⁻¹ :=
id                      
typ                     
1233  mv_power_series.inv_of_unit_eq' φ _ h
id                                   
typ                                  
1234  
1235  @[simp] protected lemma mul_inv (φ : power_series α) (h : constant_coeff α φ ≠ 0) :
id                                          └┘  └┘                          
src                                         └┘  └┘  
typ                                         └┘  └┘                          
doc    └──┘                                 └┘  └┘  
1236    φ * φ⁻¹ = 1 :=
id        
typ       
1237  mv_power_series.mul_inv φ h
id                           
typ                          
1238  
1239  @[simp] protected lemma inv_mul (φ : power_series α) (h : constant_coeff α φ ≠ 0) :
id                                         └┘  └┘  └┘                         
src                                        └┘  └┘  └┘
typ                                        └┘  └┘  └┘                         
doc    └──┘                                └┘  └┘  └┘
1240    φ⁻¹ * φ = 1 :=
id          
typ         
1241  mv_power_series.inv_mul φ h
id                           
typ                          
1242  
1243  end discrete_field
1244  
1245  end power_series
1246  
1247  namespace power_series
1248  variable {α : Type*}
1249  
1250  local attribute [instance, priority 1] classical.prop_decidable
1251  noncomputable theory
1252  
1253  section order_basic
1254  open multiplicity
1255  variables [comm_semiring α]
id              └┘  └──┘  └─┘
src             └┘  └──┘  └─┘
typ             └┘  └──┘  └─┘
1256  
1257  /-- The order of a formal power series `φ` is the smallest `n : enat`
1258  such that `X^n` divides `φ`. The order is `⊤` if and only if `φ = 0`. -/
1259  @[reducible] def order (φ : power_series α) : enat :=
id                                 └┘  └┘  └┘      └┘
src                                └┘  └┘  └┘       └┘
typ                                └┘  └┘  └┘      └┘
doc    └───────┘                   └┘  └┘  └┘
1260  multiplicity X φ
id                  
typ                 
1261  
1262  lemma order_finite_of_coeff_ne_zero (φ : power_series α) (h : ∃ n, coeff α n φ ≠ 0) :
id                                              └┘  └┘  └┘                    
src                                             └┘  └┘  └┘
typ                                             └┘  └┘  └┘                    
doc                                             └┘  └┘  └┘
1263    (order φ).dom :=
id            
typ           
1264  begin
1265    cases h with n h, refine ⟨n, _⟩,
id                               
typ                              
1266    rw X_pow_dvd_iff, push_neg, exact ⟨n, lt_add_one n, h⟩
id                                                      
typ                                                     
1267  end
st   └─┘
1268  
1269  /-- If the order of a formal power series is finite,
1270  then the coefficient indexed by the order is nonzero.-/
1271  lemma coeff_order (φ : power_series α) (h : (order φ).dom) :
id                            └┘  └┘  └┘               
src                           └┘  └┘  └┘
typ                           └┘  └┘  └┘               
doc                           └┘  └┘  └┘
1272    coeff α (φ.order.get h) φ ≠ 0 :=
id                           
typ                          
1273  begin
1274    have H := nat.find_spec h, contrapose! H, rw X_pow_dvd_iff,
1275    intros m hm, by_cases Hm : m < nat.find h,
id                                
typ                               
1276    { have := nat.find_min h Hm, push_neg at this,
1277      rw X_pow_dvd_iff at this, exact this m (lt_add_one m) },
id                                                          
typ                                                         
st                                                             └┘
1278    have : m = nat.find h, {linarith}, {rwa this}
id            
typ           
st                                     └┘          └─
1279  end
st   ──┘
1280  
1281  /-- If the `n`th coefficient of a formal power series is nonzero,
1282  then the order of the power series is less than or equal to `n`.-/
1283  lemma order_le (φ : power_series α) (n : ℕ) (h : coeff α n φ ≠ 0) :
id                         └┘  └┘  └┘                        
src                        └┘  └┘  └┘
typ                        └┘  └┘  └┘                        
doc                        └┘  └┘  └┘
1284    order φ ≤ n :=
id              
typ             
1285  begin
1286    have h : ¬ X^(n+1) ∣ φ,
id                        
src             
typ                       
1287    { rw X_pow_dvd_iff, push_neg, exact ⟨n, lt_add_one n, h⟩ },
id                                                        
typ                                                       
st                                                              └┘
1288    have : (order φ).dom := ⟨n, h⟩,
id                             
typ                            
1289    rw [← enat.coe_get this, enat.coe_le_coe],
1290    refine nat.find_min' this h
1291  end
st   └─┘
1292  
1293  /-- The `n`th coefficient of a formal power series is `0` if `n` is strictly
1294  smaller than the order of the power series.-/
1295  lemma coeff_of_lt_order (φ : power_series α) (n : ℕ) (h: ↑n < order φ) :
id                                  └┘  └┘  └┘                         
src                                 └┘  └┘  └┘
typ                                 └┘  └┘  └┘                         
doc                                 └┘  └┘  └┘
1296    coeff α n φ = 0 :=
id             
typ            
1297  by { contrapose! h, exact order_le _ _ h }
st                                            └┘
1298  
1299  /-- The `0` power series is the unique power series with infinite order.-/
1300  lemma order_eq_top {φ : power_series α} :
id                             └┘  └┘  └┘ 
src                            └┘  └┘  └┘
typ                            └┘  └┘  └┘ 
doc                            └┘  └┘  └┘
1301    φ.order = ⊤ ↔ φ = 0 :=
id                  
src                
typ                 
1302  begin
1303    rw eq_top_iff,
1304    split,
1305    { intro h, ext n, specialize h (n+1), rw X_pow_dvd_iff at h, exact h n (lt_add_one _) },
id                                                                         
typ                                                                        
st                                                                                           └┘
1306    { rintros rfl n, exact dvd_zero _ }
st                                       └─
1307  end
st   ──┘
1308  
1309  /-- The order of the `0` power series is infinite.-/
1310  @[simp] lemma order_zero : order (0 : power_series α) = ⊤ :=
id                                         └┘  └┘  └┘   
src                                        └┘  └┘  └┘
typ                                        └┘  └┘  └┘   
doc    └──┘                                └┘  └┘  └┘
1311  multiplicity.zero _
1312  
1313  /-- The order of a formal power series is at least `n` if
1314  the `i`th coefficient is `0` for all `i < n`.-/
1315  lemma order_ge_nat (φ : power_series α) (n : ℕ) (h : ∀ i < n, coeff α i φ = 0) :
id                             └┘  └┘  └┘                               
src                            └┘  └┘  └┘
typ                            └┘  └┘  └┘                               
doc                            └┘  └┘  └┘
1316    order φ ≥ n :=
id              
typ             
1317  begin
1318    by_contra H, rw not_le at H,
1319    have : (order φ).dom := enat.dom_of_le_some (le_of_lt H),
id                   
typ                  
1320    rw [← enat.coe_get this, enat.coe_lt_coe] at H,
1321    exact coeff_order _ this (h _ H)
1322  end
st   └─┘
1323  
1324  /-- The order of a formal power series is at least `n` if
1325  the `i`th coefficient is `0` for all `i < n`.-/
1326  lemma order_ge (φ : power_series α) (n : enat) (h : ∀ i : ℕ, ↑i < n → coeff α i φ = 0) :
id                         └┘  └┘  └┘         └─┘                              
src                        └┘  └┘  └┘          └─┘             
typ                        └┘  └┘  └┘         └─┘                              
doc                        └┘  └┘  └┘
1327    order φ ≥ n :=
id              
typ             
1328  begin
1329    induction n using enat.cases_on,
1330    { show _ ≤ _, rw [lattice.top_le_iff, order_eq_top],
1331      ext i, exact h _ (enat.coe_lt_top i) },
id                                         
typ                                        
st                                            └┘
1332    { apply order_ge_nat, simpa only [enat.coe_lt_coe] using h }
st                                                                └─
1333  end
st   ──┘
1334  
1335  /-- The order of a formal power series is exactly `n` if the `n`th coefficient is nonzero,
1336  and the `i`th coefficient is `0` for all `i < n`.-/
1337  lemma order_eq_nat {φ : power_series α} {n : ℕ} :
id                             └┘  └┘  └┘ 
src                            └┘  └┘  └┘
typ                            └┘  └┘  └┘ 
doc                            └┘  └┘  └┘
1338    order φ = n ↔ (coeff α n φ ≠ 0) ∧ (∀ i, i < n → coeff α i φ = 0) :=
id                                                   
src                                   
typ                                                  
1339  begin
1340    simp only [eq_some_iff, X_pow_dvd_iff], push_neg,
1341    split,
1342    { rintros ⟨h₁, m, hm₁, hm₂⟩, refine ⟨_, h₁⟩,
1343      suffices : n = m, { rwa this },
id                     
typ                    
st                                    └┘
1344      suffices : m ≥ n, { linarith },
id                     
typ                    
st                                    └┘
1345      contrapose! hm₂, exact h₁ _ hm₂ },
id                                   └─┘
typ                                  └─┘
st                                       └┘
1346    { rintros ⟨h₁, h₂⟩, exact ⟨h₂, n, lt_add_one n, h₁⟩ }
id                                                  
typ                                                 
st                                                         └─
1347  end
st   ──┘
1348  
1349  /-- The order of a formal power series is exactly `n` if the `n`th coefficient is nonzero,
1350  and the `i`th coefficient is `0` for all `i < n`.-/
1351  lemma order_eq {φ : power_series α} {n : enat} :
id                         └┘  └┘  └┘         └─┘
src                        └┘  └┘  └┘          └─┘
typ                        └┘  └┘  └┘         └─┘
doc                        └┘  └┘  └┘
1352    order φ = n ↔ (∀ i:ℕ, ↑i = n → coeff α i φ ≠ 0) ∧ (∀ i:ℕ, ↑i < n → coeff α i φ = 0) :=
id                                                                   
src                                                         
typ                                                                  
1353  begin
1354    induction n using enat.cases_on,
id               
typ              
1355    { rw order_eq_top, split,
1356      { rintro rfl, split; intros,
1357        { exfalso, exact enat.coe_ne_top ‹_› ‹_› },
st                                                  └┘
1358        { exact (coeff _ _).map_zero } },
st                                      └──┘
1359      { rintro ⟨h₁, h₂⟩, ext i, exact h₂ i (enat.coe_lt_top i) } },
id                                                             
typ                                                            
st                                                                └──┘
1360    { simpa [enat.coe_inj] using order_eq_nat }
st                                               └─
1361  end
st   ──┘
1362  
1363  /-- The order of the sum of two formal power series
1364   is at least the minimum of their orders.-/
1365  lemma order_add_ge (φ ψ : power_series α) :
id                                          
typ                                         
1366    order (φ + ψ) ≥ min (order φ) (order ψ) :=
id                                       
typ                                      
1367  multiplicity.min_le_multiplicity_add
1368  
1369  private lemma order_add_of_order_eq.aux (φ ψ : power_series α)
id                                                               
typ                                                              
1370    (h : order φ ≠ order ψ) (H : order φ < order ψ) :
id                                               
typ                                              
1371    order (φ + ψ) ≤ order φ ⊓ order ψ :=
id                                  
typ                                 
1372  begin
1373    suffices : order (φ + ψ) = order φ,
id                                     
typ                                    
1374    { rw [lattice.le_inf_iff, this], exact ⟨le_refl _, le_of_lt H⟩ },
st                                                                    └┘
1375    { rw order_eq, split,
1376      { intros i hi, rw [(coeff _ _).map_add, coeff_of_lt_order ψ i (hi.symm ▸ H), add_zero],
id                                                                  
typ                                                                 
1377        exact (order_eq_nat.1 hi.symm).1 },
st                                          └┘
1378      { intros i hi,
1379        rw [(coeff _ _).map_add, coeff_of_lt_order φ i hi,
id                                                     
typ                                                    
1380          coeff_of_lt_order ψ i (lt_trans hi H), zero_add] } }
id                              
typ                             
st                                                           └───
1381  end
st   ──┘
1382  
1383  /-- The order of the sum of two formal power series
1384   is the minimum of their orders if their orders differ.-/
1385  lemma order_add_of_order_eq (φ ψ : power_series α) (h : order φ ≠ order ψ) :
id                                                                         
typ                                                                        
1386    order (φ + ψ) = order φ ⊓ order ψ :=
id                                  
typ                                 
1387  begin
1388    refine le_antisymm _ (order_add_ge _ _),
1389    by_cases H₁ : order φ < order ψ,
id                                  
typ                                 
1390    { apply order_add_of_order_eq.aux _ _ h H₁ },
st                                                └┘
1391    by_cases H₂ : order ψ < order φ,
id                                  
typ                                 
1392    { simpa only [add_comm, lattice.inf_comm] using order_add_of_order_eq.aux _ _ h.symm H₂ },
st                                                                                             └┘
1393    exfalso, exact h (le_antisymm (not_lt.1 H₂) (not_lt.1 H₁))
1394  end
st   └─┘
1395  
1396  /-- The order of the product of two formal power series
1397   is at least the sum of their orders.-/
1398  lemma order_mul_ge (φ ψ : power_series α) :
id                                          
typ                                         
1399    order (φ * ψ) ≥ order φ + order ψ :=
id                                  
typ                                 
1400  begin
1401    apply order_ge,
1402    intros n hn, rw [coeff_mul, finset.sum_eq_zero],
1403    rintros ⟨i,j⟩ hij,
1404    by_cases hi : ↑i < order φ,
id                             
typ                            
1405    { rw [coeff_of_lt_order φ i hi, zero_mul] },
id                              
typ                             
st                                              └┘
1406    by_cases hj : ↑j < order ψ,
id                             
typ                            
1407    { rw [coeff_of_lt_order ψ j hj, mul_zero] },
id                              
typ                             
st                                              └┘
1408    rw not_lt at hi hj, rw finset.nat.mem_antidiagonal at hij,
1409    exfalso,
1410    apply ne_of_lt (lt_of_lt_of_le hn $ add_le_add' hi hj),
1411    rw [← enat.coe_add, hij]
st                            
1412  end
st   └─┘
1413  
1414  /-- The order of the monomial `a*X^n` is infinite if `a = 0` and `n` otherwise.-/
1415  lemma order_monomial (n : ℕ) (a : α) :
id                                    
src                            
typ                                   
1416    order (monomial α n a) = if a = 0 then ⊤ else n :=
id                                               
typ                                              
1417  begin
1418    split_ifs with h,
1419    { rw [h, order_eq_top, add_monoid_hom.map_zero] },
st                                                    └┘
1420    { rw [order_eq], split; intros i hi,
1421      { rw [enat.coe_inj] at hi, rwa [hi, coeff_monomial'] },
st                                                            └┘
1422      { rw [enat.coe_lt_coe] at hi, rw [coeff_monomial, if_neg], exact ne_of_lt hi } }
id                                                                                 └┘
typ                                                                                └┘
st                                                                                    └───
1423  end
st   ──┘
1424  
1425  /-- The order of the monomial `a*X^n` is `n` if `a ≠ 0`.-/
1426  lemma order_monomial_of_ne_zero (n : ℕ) (a : α) (h : a ≠ 0) :
id                                                      
src                                       
typ                                                     
1427    order (monomial α n a) = n :=
id                           
typ                          
1428  by rw [order_monomial, if_neg h]
1429  
1430  end order_basic
1431  
1432  section order_zero_ne_one
1433  variables [nonzero_comm_ring α]
id              └┘  └──┘  └──┘  
src             └┘  └──┘  └──┘  
typ             └┘  └──┘  └──┘  
doc             └┘  └──┘  └──┘  
1434  
1435  /-- The order of the formal power series `1` is `0`.-/
1436  @[simp] lemma order_one : order (1 : power_series α) = 0 :=
id                                        └┘  └┘  └┘   
src                                       └┘  └┘  └┘
typ                                       └┘  └┘  └┘   
doc    └──┘                               └┘  └┘  └┘
1437  by simpa using order_monomial_of_ne_zero 0 (1:α) one_ne_zero
id                                                 
typ                                                
1438  
1439  /-- The order of the formal power series `X` is `1`.-/
1440  @[simp] lemma order_X : order (X : power_series α) = 1 :=
id                                      └┘  └┘  └┘   
src                                     └┘  └┘  └┘
typ                                     └┘  └┘  └┘   
doc    └──┘                             └┘  └┘  └┘
1441  order_monomial_of_ne_zero 1 (1:α) one_ne_zero
id                                  
typ                                 
1442  
1443  /-- The order of the formal power series `X^n` is `n`.-/
1444  @[simp] lemma order_X_pow (n : ℕ) : order ((X : power_series α)^n) = n :=
id                                                  └┘  └┘  └┘         
src                                                 └┘  └┘  └┘
typ                                                 └┘  └┘  └┘         
doc    └──┘                                          └┘  └┘  └┘
1445  by { rw [X_pow_eq, order_monomial_of_ne_zero], exact one_ne_zero }
st                                                                    └┘
1446  
1447  end order_zero_ne_one
1448  
1449  section order_integral_domain
1450  variables [integral_domain α]
id              └┘  └──┘  └──┘
src             └┘  └──┘  └──┘
typ             └┘  └──┘  └──┘
1451  
1452  /-- The order of the product of two formal power series over an integral domain
1453   is the sum of their orders.-/
1454  lemma order_mul (φ ψ : power_series α) :
id                                       
typ                                      
1455    order (φ * ψ) = order φ + order ψ :=
id                                  
typ                                 
1456  multiplicity.mul (X_prime)
1457  
1458  end order_integral_domain
1459  
1460  end power_series
1461  
1462  namespace polynomial
1463  open finsupp
1464  variables {σ : Type*} {α : Type*} [comm_semiring α]
id                                      └─┘ └─┘ └─┘ 
src                                     └─┘ └─┘ └─┘ 
typ                                     └─┘ └─┘ └─┘ 
1465  
1466  /-- The natural inclusion from polynomials into formal power series.-/
1467  instance coe_to_power_series : has_coe (polynomial α) (power_series α) :=
id                                                         └─┘  └┘  └┘  
src                                                         └─┘  └┘  └┘
typ                                                        └─┘  └┘  └┘  
doc                                                         └─┘  └┘  └┘
1468  ⟨λ φ, power_series.mk $ λ n, coeff φ n⟩
id                                      
typ                                     
1469  
1470  @[simp, elim_cast] lemma coeff_coe (φ : polynomial α) (n) :
id                                                      
typ                                                     
doc    └──┘  └───────┘
1471    power_series.coeff α n φ = coeff φ n :=
id                                    
typ                                   
1472  congr_arg (coeff φ) (finsupp.single_eq_same)
id                    
typ                   
1473  
1474  @[reducible] def monomial (n : ℕ) (a : α) : polynomial α := single n a
id                                                                    
src                                 
typ                                                                   
doc    └───────┘
1475  
1476  @[simp, elim_cast] lemma coe_monomial (n : ℕ) (a : α) :
id                                                     
src                                             
typ                                                    
doc    └──┘  └───────┘
1477    (monomial n a : power_series α) = power_series.monomial α n a :=
id                   └──────────┘                             
src                    └──────────┘
typ                  └──────────┘                             
doc                    └──────────┘
1478  power_series.ext $ λ m,
id                        
typ                       
1479  begin
1480    rw [coeff_coe, power_series.coeff_monomial],
1481    simp only [@eq_comm _ m n],
id                            
typ                           
1482    convert finsupp.single_apply,
1483  end
st   └─┘
1484  
1485  @[simp, elim_cast] lemma coe_zero : ((0 : polynomial α) : power_series α) = 0 := rfl
id                                                            └──────────┘ 
src                                                            └──────────┘
typ                                                           └──────────┘ 
doc    └──┘  └───────┘                                         └──────────┘
1486  
1487  @[simp, elim_cast] lemma coe_one : ((1 : polynomial α) : power_series α) = 1 :=
id                                                           └──────────┘ 
src                                                           └──────────┘
typ                                                          └──────────┘ 
doc    └──┘  └───────┘                                        └──────────┘
1488  begin
1489    have := coe_monomial 0 (1:α),
id                               
typ                              
1490    rwa power_series.monomial_zero_eq_C_apply at this,
1491  end
st   └─┘
1492  
1493  @[simp, elim_cast] lemma coe_add (φ ψ : polynomial α) :
id                                                      
typ                                                     
doc    └──┘  └───────┘
1494    ((φ + ψ : polynomial α) : power_series α) = φ + ψ := rfl
id                            └──────────┘        
src                              └──────────┘
typ                           └──────────┘        
doc                              └──────────┘
1495  
1496  @[simp, elim_cast] lemma coe_mul (φ ψ : polynomial α) :
id                                                      
typ                                                     
doc    └──┘  └───────┘
1497    ((φ * ψ : polynomial α) : power_series α) = φ * ψ :=
id                            └──────────┘        
src                              └──────────┘
typ                           └──────────┘        
doc                              └──────────┘
1498  power_series.ext $ λ n,
id                        
typ                       
1499  by simp only [coeff_coe, power_series.coeff_mul, coeff_mul]
1500  
1501  @[simp, elim_cast] lemma coe_C (a : α) :
id                                       
typ                                      
doc    └──┘  └───────┘
1502    ((C a : polynomial α) : power_series α) = power_series.C α a :=
id                           └──────────┘                     
src                            └──────────┘
typ                          └──────────┘                     
doc                            └──────────┘
1503  begin
1504    have := coe_monomial 0 a,
id                            
typ                           
1505    rwa power_series.monomial_zero_eq_C_apply at this,
1506  end
st   └─┘
1507  
1508  @[simp, elim_cast] lemma coe_X :
doc    └──┘  └───────┘
1509    ((X : polynomial α) : power_series α) = power_series.X :=
id                          └──────────┘ 
src                          └──────────┘
typ                         └──────────┘ 
doc                          └──────────┘
1510  coe_monomial _ _
1511  
1512  namespace coe_to_mv_power_series
1513  
1514  instance : is_semiring_hom (coe : polynomial α → power_series α) :=
id                                                   └─┘  └┘  └┘  
src                                                   └─┘  └┘  └┘
typ                                                  └─┘  └┘  └┘  
doc                                                   └─┘  └┘  └┘
1515  { map_zero := coe_zero,
1516    map_one := coe_one,
1517    map_add := coe_add,
1518    map_mul := coe_mul }
1519  
1520  end coe_to_mv_power_series
1521  end polynomial